Theorems · Definition · order theory
lowerBounds
{α : Type u_1} → [LE α] → Set α → Set αThe set of lower bounds of a set.
- Defined in
- Mathlib.Order.Bounds.Defs
- Cited by
- 212 results in Mathlib
- Foundations
- Depth 4 from the axioms, rests on 10 definitions · uses no axioms
- Assumes
- LE
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.
- Setstatement and proof · cited by 53,352
- Set.ofPredproof · cited by 6,101
Cited by221
Results whose statement or proof uses this declaration.
- BddBelowproof · cited by 401
- IsGLBproof · cited by 213
- IsLeastproof · cited by 122
- IsLeast.isGLBproof · cited by 23
- mem_lowerBoundsstatement · cited by 19
- le_isGLB_iffstatement · cited by 17
- IsCompact.exists_isMinOnproof · cited by 15
- lowerBounds_mono_setstatement and proof · cited by 12
- Monotone.mem_lowerBounds_imagestatement and proof · cited by 11
- IsGLB.lowerBounds_eqstatement and proof · cited by 11
- IsCompact.bddBelowproof · cited by 8
- bddBelow_Iccproof · cited by 8
Showing the 200 most cited of 221.