Theorems · Inductive type · order theory
Lattice
Type u → Type u
A lattice is a join-semilattice which is also a meet-semilattice.
- Defined in
- Mathlib.Order.Lattice
- Cited by
- 916 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,160
Results whose statement or proof uses this declaration.
- absstatement and proof · cited by 1,814
- Set.uIccstatement and proof · cited by 393
- abs_of_nonnegstatement and proof · cited by 279
- Sublatticestatement · cited by 225
- Finpartitionstatement · cited by 199
- LatticeHomstatement · cited by 192
- BoundedLatticeHomstatement · cited by 185
- Finpartition.partsstatement and proof · cited by 184
- abs_nonnegstatement and proof · cited by 168
- mabsstatement and proof · cited by 148
- abs_of_posstatement and proof · cited by 114
- le_abs_selfstatement and proof · cited by 113
Showing the 200 most cited of 1,160.