Theorems · Definition · order theory
Fintype.toCompleteBooleanAlgebra
(α : Type u_2) → [Fintype α] → [BooleanAlgebra α] → CompleteBooleanAlgebra α
A finite Boolean algebra is complete.
- Defined in
- Mathlib.Data.Fintype.Order
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FintypeBooleanAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypestatement and proof · cited by 7,736
- BooleanAlgebrastatement and proof · cited by 300
- CompleteBooleanAlgebrastatement · cited by 32
- CompleteDistribLatticeproof · cited by 17
- BooleanAlgebra.himp_eqproof · cited by 2
- BooleanAlgebra.sdiff_eqproof · cited by 1
- BooleanAlgebra.top_le_sup_complproof · cited by 1
- BooleanAlgebra.inf_compl_le_botproof · cited by 1
- Fintype.toCompleteDistribLatticeproof · cited by 0
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.