Theorems · Theorem · order theory

BooleanSubalgebra.mk_le_mk

∀ {α : Type u_2} [inst : BooleanAlgebra α] {L M : Sublattice α} (hL_compl : ∀ {a : α}, a ∈ L.carrier → aᶜ ∈ L.carrier)
  (hL_bot : ⊥ ∈ L.carrier) (hM_compl : ∀ {a : α}, a ∈ M.carrier → aᶜ ∈ M.carrier) (hM_bot : ⊥ ∈ M.carrier),
  { toSublattice := L, compl_mem' := hL_compl, bot_mem' := hL_bot } ≤
      { toSublattice := M, compl_mem' := hM_compl, bot_mem' := hM_bot } ↔
    L ≤ M

Defined in

Mathlib.Order.BooleanSubalgebra

Cited by

0 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

BooleanAlgebra