Theorems · Inductive type · order theory
ComplementedLattice
(α : Type u_2) → [inst : Lattice α] → [BoundedOrder α] → Prop
A complemented bounded lattice is one where every element has a (not necessarily unique) complement.
- Defined in
- Mathlib.Order.Disjoint
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- LatticeBoundedOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Latticestatement · cited by 916
- BoundedOrderstatement · cited by 270
Cited by37
Results whose statement or proof uses this declaration.
- ComplementedLattice.exists_isComplstatement and proof · cited by 15
- OrderIso.complementedLattice_iffstatement and proof · cited by 8
- IsSemisimpleModule.congrproof · cited by 6
- RingEquiv.isSemisimpleRingproof · cited by 6
- isSemisimpleModule_iffstatement and proof · cited by 5
- OrderIso.complementedLatticestatement and proof · cited by 4
- LinearMap.isSemisimpleModule_iff_of_bijectiveproof · cited by 4
- complementedLattice_of_sSup_atoms_eq_topstatement · cited by 3
- ComplementedLattice.isStronglyAtomicstatement and proof · cited by 2
- isCoatomic_of_isAtomic_of_complementedLattice_of_isModularstatement and proof · cited by 2
- complementedLattice_of_isAtomisticstatement · cited by 2
- Representation.IsSemisimpleRepresentationproof · cited by 2