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

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

Equations

• BooleanSubalgebra.instSetLike = { coe := fun (L : BooleanSubalgebra α) => L.carrier, coe_injective' := ⋯ }

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.

Equations

• L.copy s hs = { toSublattice := L.copy s ⋯, compl_mem' := ⋯, bot_mem' := ⋯ }

@[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.

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

A boolean subalgebra of a lattice inherits a bottom element.

Equations

• BooleanSubalgebra.instBotCoe = { bot := ⟨⊥, ⋯⟩ }

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

A boolean subalgebra of a lattice inherits a top element.

Equations

• BooleanSubalgebra.instTopCoe = { top := ⟨⊤, ⋯⟩ }

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

A boolean subalgebra of a lattice inherits a supremum.

Equations

• BooleanSubalgebra.instSupCoe = { max := fun (a b : ↥L) => ⟨↑a ⊔ ↑b, ⋯⟩ }

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

A boolean subalgebra of a lattice inherits an infimum.

Equations

• BooleanSubalgebra.instInfCoe = { min := fun (a b : ↥L) => ⟨↑a ⊓ ↑b, ⋯⟩ }

instance BooleanSubalgebra.instHasComplCoe {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} : HasCompl ↥L

A boolean subalgebra of a lattice inherits a complement.

Equations

• BooleanSubalgebra.instHasComplCoe = { compl := fun (a : ↥L) => ⟨(↑a)ᶜ, ⋯⟩ }

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

A boolean subalgebra of a lattice inherits a difference.

Equations

• BooleanSubalgebra.instSDiffCoe = { sdiff := fun (a b : ↥L) => ⟨↑a \ ↑b, ⋯⟩ }

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

A boolean subalgebra of a lattice inherits a Heyting implication.

Equations

• BooleanSubalgebra.instHImpCoe = { himp := fun (a b : ↥L) => ⟨↑a ⇨ ↑b, ⋯⟩ }

@[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, ⋯⟩

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

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

Equations

• L.instBooleanAlgebraCoe = Function.Injective.booleanAlgebra (fun (a : ↥L) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

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

Equations

• L.subtype = { toFun := Subtype.val, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }

@[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.

Equations

• BooleanSubalgebra.inclusion h = { toFun := Set.inclusion h, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

The maximum boolean subalgebra of a lattice.

Equations

• BooleanSubalgebra.instTop = { top := { carrier := Set.univ, supClosed' := ⋯, infClosed' := ⋯, compl_mem' := ⋯, bot_mem' := ⋯ } }

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

The trivial boolean subalgebra of a lattice.

Equations

• BooleanSubalgebra.instBot = { bot := { carrier := {⊥, ⊤}, supClosed' := ⋯, infClosed' := ⋯, compl_mem' := ⋯, bot_mem' := ⋯ } }

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

The inf of two boolean subalgebras is their intersection.

Equations

• BooleanSubalgebra.instInf = { min := fun (L M : BooleanSubalgebra α) => { carrier := ↑L ∩ ↑M, supClosed' := ⋯, infClosed' := ⋯, compl_mem' := ⋯, bot_mem' := ⋯ } }

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

The inf of boolean subalgebras is their intersection.

Equations

• BooleanSubalgebra.instInfSet = { sInf := fun (S : Set (BooleanSubalgebra α)) => { carrier := ⋂ L ∈ S, ↑L, supClosed' := ⋯, infClosed' := ⋯, compl_mem' := ⋯, bot_mem' := ⋯ } }

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

Equations

• BooleanSubalgebra.instInhabited = { default := ⊥ }

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 α.

Equations

• BooleanSubalgebra.topEquiv = { toEquiv := Equiv.Set.univ α, map_rel_iff' := ⋯ }

@[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

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

BooleanSubalgebras of a lattice form a complete lattice.

Equations

• BooleanSubalgebra.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

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

Equations

• BooleanSubalgebra.instUniqueOfIsEmpty = uniqueOfSubsingleton ⊤

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.

Equations

• BooleanSubalgebra.comap f L = { carrier := ⇑f ⁻¹' ↑L, supClosed' := ⋯, infClosed' := ⋯, compl_mem' := ⋯, bot_mem' := ⋯ }

@[simp]

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

@[simp]

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

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

@[simp]

theorem BooleanSubalgebra.comap_id {α : Type u_2} [BooleanAlgebra α] (L : BooleanSubalgebra α) : 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 α β) : BooleanSubalgebra.comap f (BooleanSubalgebra.comap g L) = BooleanSubalgebra.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.

Equations

• BooleanSubalgebra.map f L = { carrier := ⇑f '' ↑L, supClosed' := ⋯, infClosed' := ⋯, compl_mem' := ⋯, bot_mem' := ⋯ }

@[simp]

theorem BooleanSubalgebra.coe_map {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (f : BoundedLatticeHom α β) (L : BooleanSubalgebra α) : ↑(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 ∈ BooleanSubalgebra.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 ∈ BooleanSubalgebra.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 ∈ BooleanSubalgebra.map f L

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

@[simp]

theorem BooleanSubalgebra.map_id {α : Type u_2} [BooleanAlgebra α] {L : BooleanSubalgebra α} : 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 α β) : BooleanSubalgebra.map g (BooleanSubalgebra.map f L) = BooleanSubalgebra.map (g.comp f) L

theorem BooleanSubalgebra.mem_map_equiv {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] {L : BooleanSubalgebra α} {f : α ≃o β} {a : β} : a ∈ BooleanSubalgebra.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 ∈ BooleanSubalgebra.map f L ↔ a ∈ L

theorem BooleanSubalgebra.map_equiv_eq_comap_symm {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (f : α ≃o β) (L : BooleanSubalgebra α) : BooleanSubalgebra.map (let __src := { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) L = BooleanSubalgebra.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 α) : BooleanSubalgebra.comap (let __src := { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) L = BooleanSubalgebra.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 α} : BooleanSubalgebra.map (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) L = M ↔ L = BooleanSubalgebra.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 β} : BooleanSubalgebra.map f L ≤ M ↔ L ≤ BooleanSubalgebra.comap f M

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

@[simp]

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

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

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

@[simp]

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

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

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

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

theorem BooleanSubalgebra.le_comap_sup {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (L M : BooleanSubalgebra β) (f : BoundedLatticeHom α β) : BooleanSubalgebra.comap f L ⊔ BooleanSubalgebra.comap f M ≤ BooleanSubalgebra.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 : ι), BooleanSubalgebra.comap f (L i) ≤ BooleanSubalgebra.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) : BooleanSubalgebra.map f (L ⊓ M) = BooleanSubalgebra.map f L ⊓ BooleanSubalgebra.map f M

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

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

The minimum boolean subalgebra containing a given set.

Equations

• BooleanSubalgebra.closure s = sInf {L : BooleanSubalgebra α | s ⊆ ↑L}

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

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

@[simp]

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

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

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

@[simp]

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

theorem BooleanSubalgebra.closure_bot_sup_induction {α : Type u_2} [BooleanAlgebra α] {s : Set α} {p : (g : α) → g ∈ BooleanSubalgebra.closure s → Prop} (mem : ∀ (x : α) (hx : x ∈ s), p x ⋯) (bot : p ⊥ ⋯) (sup : ∀ (x : α) (hx : x ∈ BooleanSubalgebra.closure s) (y : α) (hy : y ∈ BooleanSubalgebra.closure s), p x hx → p y hy → p (x ⊔ y) ⋯) (compl : ∀ (x : α) (hx : x ∈ BooleanSubalgebra.closure s), p x hx → p xᶜ ⋯) {x : α} (hx : x ∈ BooleanSubalgebra.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 ∈ BooleanSubalgebra.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 ∈ BooleanSubalgebra.closure s → Prop} (sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯) (sup : ∀ (x : α) (hx : x ∈ BooleanSubalgebra.closure s) (y : α) (hy : y ∈ BooleanSubalgebra.closure s), p x hx → p y hy → p (x ⊔ y) ⋯) (x : α) (hx : x ∈ BooleanSubalgebra.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