Theorems · Inductive type · order theory
SemilatticeInf
Type u → Type u
A SemilatticeInf is a meet-semilattice, that is, a partial order
with a meet (a.k.a. glb / greatest lower bound, inf / infimum) operation
⊓ which is the greatest element smaller than both factors.
- Defined in
- Mathlib.Order.Lattice
- Cited by
- 634 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 by713
Results whose statement or proof uses this declaration.
- inf_le_leftstatement and proof · cited by 286
- inf_le_rightstatement and proof · cited by 238
- Finset.infstatement and proof · cited by 219
- inf_of_le_leftstatement and proof · cited by 186
- inf_commstatement and proof · cited by 139
- inf_of_le_rightstatement and proof · cited by 128
- Finset.inf'statement and proof · cited by 117
- le_infstatement and proof · cited by 107
- disjoint_iffstatement and proof · cited by 76
- disjoint_iff_inf_lestatement and proof · cited by 64
- inf_eq_rightstatement and proof · cited by 64
- Finset.hasInfsstatement and proof · cited by 62
Showing the 200 most cited of 713.