Boolean subalgebras

This file defines Boolean subalgebras.

structure BooleanSubalgebra (α : Type u_2) [BooleanAlgebra α] extends Sublattice α : Type u_2

A Boolean subalgebra of a Boolean algebra is a set containing the bottom and top elements, and closed under suprema, infima and complements.

• carrier : Set α
• supClosed' : SupClosed self.carrier
• infClosed' : InfClosed self.carrier
• compl_mem' {a : α} : a ∈ self.carrier → aᶜ ∈ self.carrier
• bot_mem' : ⊥ ∈ self.carrier

@[implicit_reducible]

instance BooleanSubalgebra.instSetLike {α : Type u_2} [BooleanAlgebra α] : SetLike (BooleanSubalgebra α) α

@[implicit_reducible]

instance BooleanSubalgebra.instPartialOrder {α : Type u_2} [BooleanAlgebra α] : PartialOrder (BooleanSubalgebra α)

theorem BooleanSubalgebra.coe_inj {α : Type u_2} [BooleanAlgebra α] {L M : BooleanSubalgebra α} : ↑L = ↑M ↔ L = M

@[simp]

theorem BooleanSubalgebra.supClosed {α : Type u_2} [BooleanAlgebra α] (L : BooleanSubalgebra α) : SupClosed ↑L

@[simp]

theorem BooleanSubalgebra.infClosed {α : Type u_2} [BooleanAlgebra α] (L : BooleanSubalgebra α) : InfClosed ↑L

theorem BooleanSubalgebra.compl_mem {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} {a : α} (ha : a ∈ L) : aᶜ ∈ L

@[simp]

theorem BooleanSubalgebra.compl_mem_iff {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} {a : α} : aᶜ ∈ L ↔ a ∈ L

@[simp]

theorem BooleanSubalgebra.bot_mem {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} : ⊥ ∈ L

@[simp]

theorem BooleanSubalgebra.top_mem {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} : ⊤ ∈ L

theorem BooleanSubalgebra.sup_mem {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} {a b : α} (ha : a ∈ L) (hb : b ∈ L) : a ⊔ b ∈ L

theorem BooleanSubalgebra.inf_mem {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} {a b : α} (ha : a ∈ L) (hb : b ∈ L) : a ⊓ b ∈ L

theorem BooleanSubalgebra.sdiff_mem {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} {a b : α} (ha : a ∈ L) (hb : b ∈ L) : a \ b ∈ L

theorem BooleanSubalgebra.himp_mem {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} {a b : α} (ha : a ∈ L) (hb : b ∈ L) : a ⇨ b ∈ L

theorem BooleanSubalgebra.mem_carrier {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} {a : α} : a ∈ L.carrier ↔ a ∈ L

@[simp]

theorem BooleanSubalgebra.mem_toSublattice {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} {a : α} : a ∈ L.toSublattice ↔ a ∈ L

@[simp]

theorem BooleanSubalgebra.mem_mk {α : Type u_2} [BooleanAlgebra α] {a : α} {L : Sublattice α} (h_compl : ∀ {a : α}, a ∈ L.carrier → aᶜ ∈ L.carrier) (h_bot : ⊥ ∈ L.carrier) : a ∈ { toSublattice := L, compl_mem' := h_compl, bot_mem' := h_bot } ↔ a ∈ L

@[simp]

theorem BooleanSubalgebra.coe_mk {α : Type u_2} [BooleanAlgebra α] (L : Sublattice α) (h_compl : ∀ {a : α}, a ∈ L.carrier → aᶜ ∈ L.carrier) (h_bot : ⊥ ∈ L.carrier) : ↑{ toSublattice := L, compl_mem' := h_compl, bot_mem' := h_bot } = ↑L

@[simp]

theorem BooleanSubalgebra.mk_le_mk {α : Type u_2} [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

@[simp]

theorem BooleanSubalgebra.mk_lt_mk {α : Type u_2} [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

def BooleanSubalgebra.copy {α : Type u_2} [BooleanAlgebra α] (L : BooleanSubalgebra α) (s : Set α) (hs : s = ↑L) : BooleanSubalgebra α

Copy of a Boolean subalgebra with a new carrier equal to the old one. Useful to fix definitional equalities.

@[simp]

theorem BooleanSubalgebra.coe_copy {α : Type u_2} [BooleanAlgebra α] (L : BooleanSubalgebra α) (s : Set α) (hs : s = ↑L) : ↑(L.copy s hs) = s

theorem BooleanSubalgebra.copy_eq {α : Type u_2} [BooleanAlgebra α] (L : BooleanSubalgebra α) (s : Set α) (hs : s = ↑L) : L.copy s hs = L

theorem BooleanSubalgebra.ext {α : Type u_2} [BooleanAlgebra α] {L M : BooleanSubalgebra α} : (∀ (a : α), a ∈ L ↔ a ∈ M) → L = M

Two Boolean subalgebras are equal if they have the same elements.

@[implicit_reducible]

instance BooleanSubalgebra.instBotCoe {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} : Bot ↥L

A Boolean subalgebra of a lattice inherits a bottom element.

@[implicit_reducible]

instance BooleanSubalgebra.instTopCoe {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} : Top ↥L

A Boolean subalgebra of a lattice inherits a top element.

@[implicit_reducible]

instance BooleanSubalgebra.instSupCoe {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} : Max ↥L

A Boolean subalgebra of a lattice inherits a supremum.

@[implicit_reducible]

instance BooleanSubalgebra.instInfCoe {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} : Min ↥L

A Boolean subalgebra of a lattice inherits an infimum.

@[implicit_reducible]

instance BooleanSubalgebra.instComplCoe {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} : Compl ↥L

A Boolean subalgebra of a lattice inherits a complement.

@[implicit_reducible]

instance BooleanSubalgebra.instSDiffCoe {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} : SDiff ↥L

A Boolean subalgebra of a lattice inherits a difference.

@[implicit_reducible]

instance BooleanSubalgebra.instHImpCoe {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} : HImp ↥L

A Boolean subalgebra of a lattice inherits a Heyting implication.

@[simp]

theorem BooleanSubalgebra.val_bot {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} : ↑⊥ = ⊥

@[simp]

theorem BooleanSubalgebra.val_top {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} : ↑⊤ = ⊤

@[simp]

theorem BooleanSubalgebra.val_sup {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} (a b : ↥L) : ↑(a ⊔ b) = ↑a ⊔ ↑b

@[simp]

theorem BooleanSubalgebra.val_inf {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} (a b : ↥L) : ↑(a ⊓ b) = ↑a ⊓ ↑b

@[simp]

theorem BooleanSubalgebra.val_compl {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} (a : ↥L) : ↑aᶜ = (↑a)ᶜ

@[simp]

theorem BooleanSubalgebra.val_sdiff {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} (a b : ↥L) : ↑(a \ b) = ↑a \ ↑b

@[simp]

theorem BooleanSubalgebra.val_himp {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} (a b : ↥L) : ↑(a ⇨ b) = ↑a ⇨ ↑b

@[simp]

theorem BooleanSubalgebra.mk_bot {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} : ⟨⊥, ⋯⟩ = ⊥

@[simp]

theorem BooleanSubalgebra.mk_top {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} : ⟨⊤, ⋯⟩ = ⊤

@[simp]

theorem BooleanSubalgebra.mk_sup_mk {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} (a b : α) (ha : a ∈ L) (hb : b ∈ L) : ⟨a, ha⟩ ⊔ ⟨b, hb⟩ = ⟨a ⊔ b, ⋯⟩

@[simp]

theorem BooleanSubalgebra.mk_inf_mk {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} (a b : α) (ha : a ∈ L) (hb : b ∈ L) : ⟨a, ha⟩ ⊓ ⟨b, hb⟩ = ⟨a ⊓ b, ⋯⟩

@[simp]

theorem BooleanSubalgebra.compl_mk {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} (a : α) (ha : a ∈ L) : ⟨a, ha⟩ᶜ = ⟨aᶜ, ⋯⟩

@[simp]

theorem BooleanSubalgebra.mk_sdiff_mk {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} (a b : α) (ha : a ∈ L) (hb : b ∈ L) : ⟨a, ha⟩ \ ⟨b, hb⟩ = ⟨a \ b, ⋯⟩

@[simp]

theorem BooleanSubalgebra.mk_himp_mk {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} (a b : α) (ha : a ∈ L) (hb : b ∈ L) : ⟨a, ha⟩ ⇨ ⟨b, hb⟩ = ⟨a ⇨ b, ⋯⟩

@[implicit_reducible]

instance BooleanSubalgebra.instPartialOrderSubtypeMem {α : Type u_2} [BooleanAlgebra α] (L : BooleanSubalgebra α) : PartialOrder ↥L

@[implicit_reducible]

instance BooleanSubalgebra.instBooleanAlgebraCoe {α : Type u_2} [BooleanAlgebra α] (L : BooleanSubalgebra α) : BooleanAlgebra ↥L

A Boolean subalgebra of a lattice inherits a Boolean algebra structure.

def BooleanSubalgebra.subtype {α : Type u_2} [BooleanAlgebra α] (L : BooleanSubalgebra α) : BoundedLatticeHom (↥L) α

The natural lattice hom from a Boolean subalgebra to the original lattice.

@[simp]

theorem BooleanSubalgebra.coe_subtype {α : Type u_2} [BooleanAlgebra α] (L : BooleanSubalgebra α) : ⇑L.subtype = Subtype.val

theorem BooleanSubalgebra.subtype_apply {α : Type u_2} [BooleanAlgebra α] (L : BooleanSubalgebra α) (a : ↥L) : L.subtype a = ↑a

theorem BooleanSubalgebra.subtype_injective {α : Type u_2} [BooleanAlgebra α] (L : BooleanSubalgebra α) : Function.Injective ⇑L.subtype

def BooleanSubalgebra.inclusion {α : Type u_2} [BooleanAlgebra α] {L M : BooleanSubalgebra α} (h : L ≤ M) : BoundedLatticeHom ↥L ↥M

The inclusion homomorphism from a Boolean subalgebra L to a bigger Boolean subalgebra M.

@[simp]

theorem BooleanSubalgebra.coe_inclusion {α : Type u_2} [BooleanAlgebra α] {L M : BooleanSubalgebra α} (h : L ≤ M) : ⇑(inclusion h) = Set.inclusion h

theorem BooleanSubalgebra.inclusion_apply {α : Type u_2} [BooleanAlgebra α] {L M : BooleanSubalgebra α} (h : L ≤ M) (a : ↥L) : (inclusion h) a = Set.inclusion h a

theorem BooleanSubalgebra.inclusion_injective {α : Type u_2} [BooleanAlgebra α] {L M : BooleanSubalgebra α} (h : L ≤ M) : Function.Injective ⇑(inclusion h)

@[simp]

theorem BooleanSubalgebra.inclusion_rfl {α : Type u_2} [BooleanAlgebra α] (L : BooleanSubalgebra α) : inclusion ⋯ = BoundedLatticeHom.id ↥L

@[simp]

theorem BooleanSubalgebra.subtype_comp_inclusion {α : Type u_2} [BooleanAlgebra α] {L M : BooleanSubalgebra α} (h : L ≤ M) : M.subtype.comp (inclusion h) = L.subtype

@[implicit_reducible]

instance BooleanSubalgebra.instTop {α : Type u_2} [BooleanAlgebra α] : Top (BooleanSubalgebra α)

The maximum Boolean subalgebra of a lattice.

@[implicit_reducible]

instance BooleanSubalgebra.instBot {α : Type u_2} [BooleanAlgebra α] : Bot (BooleanSubalgebra α)

The trivial Boolean subalgebra of a lattice.

@[implicit_reducible]

instance BooleanSubalgebra.instInf {α : Type u_2} [BooleanAlgebra α] : Min (BooleanSubalgebra α)

The inf of two Boolean subalgebras is their intersection.

@[implicit_reducible]

instance BooleanSubalgebra.instInfSet {α : Type u_2} [BooleanAlgebra α] : InfSet (BooleanSubalgebra α)

The inf of Boolean subalgebras is their intersection.

@[implicit_reducible]

instance BooleanSubalgebra.instInhabited {α : Type u_2} [BooleanAlgebra α] : Inhabited (BooleanSubalgebra α)

def BooleanSubalgebra.topEquiv {α : Type u_2} [BooleanAlgebra α] : ↥⊤ ≃o α

The top Boolean subalgebra is isomorphic to the original Boolean algebra.

This is the Boolean subalgebra version of Equiv.Set.univ α.

@[simp]

theorem BooleanSubalgebra.coe_top {α : Type u_2} [BooleanAlgebra α] : ↑⊤ = Set.univ

@[simp]

theorem BooleanSubalgebra.coe_bot {α : Type u_2} [BooleanAlgebra α] : ↑⊥ = {⊥, ⊤}

@[simp]

theorem BooleanSubalgebra.coe_inf {α : Type u_2} [BooleanAlgebra α] (L M : BooleanSubalgebra α) : ↑(L ⊓ M) = ↑L ∩ ↑M

@[simp]

theorem BooleanSubalgebra.coe_sInf {α : Type u_2} [BooleanAlgebra α] (S : Set (BooleanSubalgebra α)) : ↑(sInf S) = ⋂ L ∈ S, ↑L

@[simp]

theorem BooleanSubalgebra.coe_iInf {ι : Sort u_1} {α : Type u_2} [BooleanAlgebra α] (f : ι → BooleanSubalgebra α) : ↑(⨅ (i : ι), f i) = ⋂ (i : ι), ↑(f i)

@[simp]

theorem BooleanSubalgebra.coe_eq_univ {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} : ↑L = Set.univ ↔ L = ⊤

@[simp]

theorem BooleanSubalgebra.mem_bot {α : Type u_2} [BooleanAlgebra α] {a : α} : a ∈ ⊥ ↔ a = ⊥ ∨ a = ⊤

@[simp]

theorem BooleanSubalgebra.mem_top {α : Type u_2} [BooleanAlgebra α] {a : α} : a ∈ ⊤

@[simp]

theorem BooleanSubalgebra.mem_inf {α : Type u_2} [BooleanAlgebra α] {L M : BooleanSubalgebra α} {a : α} : a ∈ L ⊓ M ↔ a ∈ L ∧ a ∈ M

@[simp]

theorem BooleanSubalgebra.mem_sInf {α : Type u_2} [BooleanAlgebra α] {a : α} {S : Set (BooleanSubalgebra α)} : a ∈ sInf S ↔ ∀ L ∈ S, a ∈ L

@[simp]

theorem BooleanSubalgebra.mem_iInf {ι : Sort u_1} {α : Type u_2} [BooleanAlgebra α] {a : α} {f : ι → BooleanSubalgebra α} : a ∈ ⨅ (i : ι), f i ↔ ∀ (i : ι), a ∈ f i

@[implicit_reducible]

instance BooleanSubalgebra.instCompleteLattice {α : Type u_2} [BooleanAlgebra α] : CompleteLattice (BooleanSubalgebra α)

BooleanSubalgebras of a lattice form a complete lattice.

instance BooleanSubalgebra.instSubsingletonOfIsEmpty {α : Type u_2} [BooleanAlgebra α] [IsEmpty α] : Subsingleton (BooleanSubalgebra α)

@[implicit_reducible]

instance BooleanSubalgebra.instUniqueOfIsEmpty {α : Type u_2} [BooleanAlgebra α] [IsEmpty α] : Unique (BooleanSubalgebra α)

def BooleanSubalgebra.comap {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (f : BoundedLatticeHom α β) (L : BooleanSubalgebra β) : BooleanSubalgebra α

The preimage of a Boolean subalgebra along a bounded lattice homomorphism.

@[simp]

theorem BooleanSubalgebra.coe_comap {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (L : BooleanSubalgebra β) (f : BoundedLatticeHom α β) : ↑(comap f L) = ⇑f ⁻¹' ↑L

@[simp]

theorem BooleanSubalgebra.mem_comap {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] {f : BoundedLatticeHom α β} {a : α} {L : BooleanSubalgebra β} : a ∈ comap f L ↔ f a ∈ L

theorem BooleanSubalgebra.comap_mono {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] {f : BoundedLatticeHom α β} : Monotone (comap f)

@[simp]

theorem BooleanSubalgebra.comap_id {α : Type u_2} [BooleanAlgebra α] (L : BooleanSubalgebra α) : comap (BoundedLatticeHom.id α) L = L

@[simp]

theorem BooleanSubalgebra.comap_comap {α : Type u_2} {β : Type u_3} {γ : Type u_4} [BooleanAlgebra α] [BooleanAlgebra β] [BooleanAlgebra γ] (L : BooleanSubalgebra γ) (g : BoundedLatticeHom β γ) (f : BoundedLatticeHom α β) : comap f (comap g L) = comap (g.comp f) L

def BooleanSubalgebra.map {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (f : BoundedLatticeHom α β) (L : BooleanSubalgebra α) : BooleanSubalgebra β

The image of a Boolean subalgebra along a monoid homomorphism is a Boolean subalgebra.

@[simp]

theorem BooleanSubalgebra.coe_map {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (f : BoundedLatticeHom α β) (L : BooleanSubalgebra α) : ↑(map f L) = ⇑f '' ↑L

@[simp]

theorem BooleanSubalgebra.mem_map {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] {L : BooleanSubalgebra α} {f : BoundedLatticeHom α β} {b : β} : b ∈ map f L ↔ ∃ a ∈ L, f a = b

theorem BooleanSubalgebra.mem_map_of_mem {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] {L : BooleanSubalgebra α} (f : BoundedLatticeHom α β) {a : α} : a ∈ L → f a ∈ map f L

theorem BooleanSubalgebra.apply_coe_mem_map {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] {L : BooleanSubalgebra α} (f : BoundedLatticeHom α β) (a : ↥L) : f ↑a ∈ map f L

theorem BooleanSubalgebra.map_mono {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] {f : BoundedLatticeHom α β} : Monotone (map f)

@[simp]

theorem BooleanSubalgebra.map_id {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} : map (BoundedLatticeHom.id α) L = L

@[simp]

theorem BooleanSubalgebra.map_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [BooleanAlgebra α] [BooleanAlgebra β] [BooleanAlgebra γ] {L : BooleanSubalgebra α} (g : BoundedLatticeHom β γ) (f : BoundedLatticeHom α β) : map g (map f L) = map (g.comp f) L

theorem BooleanSubalgebra.mem_map_equiv {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] {L : BooleanSubalgebra α} {f : α ≃o β} {a : β} : a ∈ map (let __src := { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) L ↔ f.symm a ∈ L

theorem BooleanSubalgebra.apply_mem_map_iff {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] {L : BooleanSubalgebra α} {f : BoundedLatticeHom α β} {a : α} (hf : Function.Injective ⇑f) : f a ∈ map f L ↔ a ∈ L

theorem BooleanSubalgebra.map_equiv_eq_comap_symm {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (f : α ≃o β) (L : BooleanSubalgebra α) : map (let __src := { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) L = comap (let __src := { toFun := ⇑f.symm, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑f.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) L

theorem BooleanSubalgebra.comap_equiv_eq_map_symm {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (f : β ≃o α) (L : BooleanSubalgebra α) : comap (let __src := { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) L = map (let __src := { toFun := ⇑f.symm, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑f.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) L

theorem BooleanSubalgebra.map_symm_eq_iff_eq_map {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] {L : BooleanSubalgebra α} {M : BooleanSubalgebra β} {e : β ≃o α} : map (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) L = M ↔ L = map (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) M

theorem BooleanSubalgebra.map_le_iff_le_comap {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] {L : BooleanSubalgebra α} {f : BoundedLatticeHom α β} {M : BooleanSubalgebra β} : map f L ≤ M ↔ L ≤ comap f M

theorem BooleanSubalgebra.gc_map_comap {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (f : BoundedLatticeHom α β) : GaloisConnection (map f) (comap f)

@[simp]

theorem BooleanSubalgebra.map_bot {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (f : BoundedLatticeHom α β) : map f ⊥ = ⊥

theorem BooleanSubalgebra.map_sup {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (f : BoundedLatticeHom α β) (L M : BooleanSubalgebra α) : map f (L ⊔ M) = map f L ⊔ map f M

theorem BooleanSubalgebra.map_iSup {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (f : BoundedLatticeHom α β) (L : ι → BooleanSubalgebra α) : map f (⨆ (i : ι), L i) = ⨆ (i : ι), map f (L i)

@[simp]

theorem BooleanSubalgebra.comap_top {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (f : BoundedLatticeHom α β) : comap f ⊤ = ⊤

theorem BooleanSubalgebra.comap_inf {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (L M : BooleanSubalgebra β) (f : BoundedLatticeHom α β) : comap f (L ⊓ M) = comap f L ⊓ comap f M

theorem BooleanSubalgebra.comap_iInf {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (f : BoundedLatticeHom α β) (L : ι → BooleanSubalgebra β) : comap f (⨅ (i : ι), L i) = ⨅ (i : ι), comap f (L i)

theorem BooleanSubalgebra.map_inf_le {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (L M : BooleanSubalgebra α) (f : BoundedLatticeHom α β) : map f (L ⊓ M) ≤ map f L ⊓ map f M

theorem BooleanSubalgebra.le_comap_sup {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (L M : BooleanSubalgebra β) (f : BoundedLatticeHom α β) : comap f L ⊔ comap f M ≤ comap f (L ⊔ M)

theorem BooleanSubalgebra.le_comap_iSup {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (f : BoundedLatticeHom α β) (L : ι → BooleanSubalgebra β) : ⨆ (i : ι), comap f (L i) ≤ comap f (⨆ (i : ι), L i)

theorem BooleanSubalgebra.map_inf {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (L M : BooleanSubalgebra α) (f : BoundedLatticeHom α β) (hf : Function.Injective ⇑f) : map f (L ⊓ M) = map f L ⊓ map f M

theorem BooleanSubalgebra.map_top {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (f : BoundedLatticeHom α β) (h : Function.Surjective ⇑f) : map f ⊤ = ⊤

def BooleanSubalgebra.closure {α : Type u_2} [BooleanAlgebra α] (s : Set α) : BooleanSubalgebra α

The minimum Boolean subalgebra containing a given set.

theorem BooleanSubalgebra.mem_closure {α : Type u_2} [BooleanAlgebra α] {s : Set α} {x : α} : x ∈ closure s ↔ ∀ ⦃L : BooleanSubalgebra α⦄, s ⊆ ↑L → x ∈ L

@[simp]

theorem BooleanSubalgebra.subset_closure {α : Type u_2} [BooleanAlgebra α] {s : Set α} : s ⊆ ↑(closure s)

theorem BooleanSubalgebra.mem_closure_of_mem {α : Type u_2} [BooleanAlgebra α] {s : Set α} {x : α} (hx : x ∈ s) : x ∈ closure s

@[simp]

theorem BooleanSubalgebra.closure_le {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} {s : Set α} : closure s ≤ L ↔ s ⊆ ↑L

theorem BooleanSubalgebra.closure_mono {α : Type u_2} [BooleanAlgebra α] {t s : Set α} (hst : s ⊆ t) : closure s ≤ closure t

theorem BooleanSubalgebra.latticeClosure_subset_closure {α : Type u_2} [BooleanAlgebra α] {s : Set α} : latticeClosure s ⊆ ↑(closure s)

@[simp]

theorem BooleanSubalgebra.closure_latticeClosure {α : Type u_2} [BooleanAlgebra α] (s : Set α) : closure (latticeClosure s) = closure s

theorem BooleanSubalgebra.closure_bot_sup_induction {α : Type u_2} [BooleanAlgebra α] {s : Set α} {p : (g : α) → g ∈ closure s → Prop} (mem : ∀ (x : α) (hx : x ∈ s), p x ⋯) (bot : p ⊥ ⋯) (sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯) (compl : ∀ (x : α) (hx : x ∈ closure s), p x hx → p xᶜ ⋯) {x : α} (hx : x ∈ closure s) : p x hx

An induction principle for closure membership. If p holds for ⊥ and all elements of s, and is preserved under suprema and complement, then p holds for all elements of the closure of s.

theorem BooleanSubalgebra.mem_closure_iff_sup_sdiff {α : Type u_2} [BooleanAlgebra α] {s : Set α} (isSublattice : IsSublattice s) (bot_mem : ⊥ ∈ s) (top_mem : ⊤ ∈ s) {a : α} : a ∈ closure s ↔ ∃ (t : Finset (↑s × ↑s)), a = t.sup fun (x : ↑s × ↑s) => ↑x.1 \ ↑x.2

theorem BooleanSubalgebra.closure_sdiff_sup_induction {α : Type u_2} [BooleanAlgebra α] {s : Set α} (isSublattice : IsSublattice s) (bot_mem : ⊥ ∈ s) (top_mem : ⊤ ∈ s) {p : (g : α) → g ∈ closure s → Prop} (sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯) (sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯) (x : α) (hx : x ∈ closure s) : p x hx

theorem BooleanSubalgebra.iSup_mem {ι : Sort u_1} {α : Type u_2} [CompleteBooleanAlgebra α] {L : BooleanSubalgebra α} {f : ι → α} [Finite ι] (hf : ∀ (i : ι), f i ∈ L) : ⨆ (i : ι), f i ∈ L

theorem BooleanSubalgebra.iInf_mem {ι : Sort u_1} {α : Type u_2} [CompleteBooleanAlgebra α] {L : BooleanSubalgebra α} {f : ι → α} [Finite ι] (hf : ∀ (i : ι), f i ∈ L) : ⨅ (i : ι), f i ∈ L

theorem BooleanSubalgebra.sSup_mem {α : Type u_2} [CompleteBooleanAlgebra α] {L : BooleanSubalgebra α} {s : Set α} (hs : s.Finite) (hsL : s ⊆ ↑L) : sSup s ∈ L

theorem BooleanSubalgebra.sInf_mem {α : Type u_2} [CompleteBooleanAlgebra α] {L : BooleanSubalgebra α} {s : Set α} (hs : s.Finite) (hsL : s ⊆ ↑L) : sInf s ∈ L

theorem BooleanSubalgebra.biSup_mem {α : Type u_2} [CompleteBooleanAlgebra α] {L : BooleanSubalgebra α} {ι : Type u_5} {t : Set ι} {f : ι → α} (ht : t.Finite) (hf : ∀ i ∈ t, f i ∈ L) : ⨆ i ∈ t, f i ∈ L

theorem BooleanSubalgebra.biInf_mem {α : Type u_2} [CompleteBooleanAlgebra α] {L : BooleanSubalgebra α} {ι : Type u_5} {t : Set ι} {f : ι → α} (ht : t.Finite) (hf : ∀ i ∈ t, f i ∈ L) : ⨅ i ∈ t, f i ∈ L