Theorems · Definition · order theory
IsBot
{α : Type u_1} → [LE α] → α → Propa : α is a bottom element of α if it is less than or equal to any other element of α.
This predicate is roughly an unbundled version of OrderBot, except that a preorder may have
several bottom elements. When α is linear, this is useful to make a case disjunction on
NoMinOrder α within a proof.
- Defined in
- Mathlib.Order.Max
- Cited by
- 77 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- LE
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 by84
Results whose statement or proof uses this declaration.
- botSetproof · cited by 16
- BoundedVariationOn.vectorMeasureproof · cited by 11
- isBot_botstatement · cited by 9
- IsBot.isMinstatement and proof · cited by 7
- Antitone.map_limsSup_of_continuousAtproof · cited by 6
- StieltjesFunction.measure_singletonproof · cited by 6
- leftLim_eq_of_isBotstatement and proof · cited by 5
- Set.subsingleton_isBotstatement and proof · cited by 5
- Dense.exists_le'statement and proof · cited by 4
- not_isBotstatement and proof · cited by 4
- IsMin.isBotstatement · cited by 4
- Dense.borel_eq_generateFrom_Ico_mem_auxstatement and proof · cited by 3