Theorems · Inductive type · order theory
CompleteLattice
Type u_8 → Type u_8
A complete lattice is a bounded lattice which has suprema and infima for every subset.
- Defined in
- Mathlib.Order.CompleteLattice.Defs
- Cited by
- 1,048 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by1,252
Results whose statement or proof uses this declaration.
- le_iSupstatement and proof · cited by 207
- iSup_lestatement and proof · cited by 190
- iInf_lestatement and proof · cited by 104
- le_iInfstatement and proof · cited by 102
- iSupIndepstatement and proof · cited by 100
- iSup₂_lestatement and proof · cited by 96
- Partitionstatement · cited by 91
- le_iSup_of_lestatement and proof · cited by 79
- GaloisConnection.l_iSupstatement and proof · cited by 78
- FrameHomstatement · cited by 70
- CompleteSublatticestatement · cited by 69
- le_iInf₂statement and proof · cited by 67
Showing the 200 most cited of 1,252.