Boolean subalgebras from complement and meet closure

A subset s : Set α of a Boolean algebra containing ⊥ and closed under complement (ᶜ) and meet (⊓) is also closed under join (⊔) by De Morgan's law (x ⊔ y = (xᶜ ⊓ yᶜ)ᶜ), and therefore forms a BooleanSubalgebra α (BooleanSubalgebra.ofComplInf). Every BooleanSubalgebra is also closed under symmetric difference (BooleanSubalgebra.symmDiff_mem).

Main definitions

• BooleanSubalgebra.ofComplInf: construct a BooleanSubalgebra from ⊥, complement, and meet closure.

Main results

• BooleanSubalgebra.coe_ofComplInf, BooleanSubalgebra.mem_ofComplInf: @[simp] carrier and membership lemmas for BooleanSubalgebra.ofComplInf.
• BooleanSubalgebra.symmDiff_mem: closure of any BooleanSubalgebra under symmetric difference.

def BooleanSubalgebra.ofComplInf {α : Type u_1} [BooleanAlgebra α] (s : Set α) (hbot : ⊥ ∈ s) (hcompl : ∀ ⦃x : α⦄, x ∈ s → xᶜ ∈ s) (hinf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → x ⊓ y ∈ s) : BooleanSubalgebra α

Construct a BooleanSubalgebra from closure under ⊥, complement, and meet (⊓), deriving join (⊔) closure by De Morgan's law (x ⊔ y = (xᶜ ⊓ yᶜ)ᶜ).

@[simp]

theorem BooleanSubalgebra.coe_ofComplInf {α : Type u_1} [BooleanAlgebra α] (s : Set α) (hbot : ⊥ ∈ s) (hcompl : ∀ ⦃x : α⦄, x ∈ s → xᶜ ∈ s) (hinf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → x ⊓ y ∈ s) : ↑(ofComplInf s hbot hcompl hinf) = s

The underlying set of ofComplInf s hbot hcompl hinf is s.

@[simp]

theorem BooleanSubalgebra.mem_ofComplInf {α : Type u_1} [BooleanAlgebra α] {s : Set α} {hbot : ⊥ ∈ s} {hcompl : ∀ ⦃x : α⦄, x ∈ s → xᶜ ∈ s} {hinf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → x ⊓ y ∈ s} {x : α} : x ∈ ofComplInf s hbot hcompl hinf ↔ x ∈ s

Membership in ofComplInf s hbot hcompl hinf is membership in s.

theorem BooleanSubalgebra.symmDiff_mem {α : Type u_1} [BooleanAlgebra α] (S : BooleanSubalgebra α) {x y : α} (hx : x ∈ S) (hy : y ∈ S) : symmDiff x y ∈ S

Every BooleanSubalgebra is closed under symmetric difference x ∆ y = (x \ y) ⊔ (y \ x).