Theorems · Inductive type · order theory
BooleanSubalgebra
(α : Type u_2) → [BooleanAlgebra α] → 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.
- Defined in
- Mathlib.Order.BooleanSubalgebra
- Cited by
- 104 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- BooleanAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- BooleanAlgebrastatement · cited by 300
Cited by118
Results whose statement or proof uses this declaration.
- BooleanSubalgebra.mapstatement and proof · cited by 20
- BooleanSubalgebra.comapstatement and proof · cited by 14
- BooleanSubalgebra.closurestatement and proof · cited by 12
- BooleanSubalgebra.subset_closurestatement and proof · cited by 9
- BooleanSubalgebra.bot_memstatement and proof · cited by 7
- BooleanSubalgebra.infClosedstatement and proof · cited by 7
- BooleanSubalgebra.supClosedstatement and proof · cited by 7
- BooleanSubalgebra.toSublatticestatement and proof · cited by 7
- BooleanSubalgebra.compl_memstatement and proof · cited by 6
- BooleanSubalgebra.gc_map_comapstatement and proof · cited by 6
- BooleanSubalgebra.inclusionstatement and proof · cited by 5
- BooleanSubalgebra.sdiff_memstatement and proof · cited by 5