Theorems · Theorem · order theory
not_isBot
∀ {α : Type u_1} [inst : LE α] [NoBotOrder α] (a : α), ¬IsBot a- Defined in
- Mathlib.Order.Max
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- LENoBotOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- IsBotstatement and proof · cited by 77
- NoBotOrderstatement and proof · cited by 43
- NoBotOrder.exists_not_geproof · cited by 5
Cited by4
Results whose statement or proof uses this declaration.
- WithBot.forall_coe_le_iff_leproof · cited by 1
- NoBotOrder.lowerBounds_univproof · cited by 1
- WithBot.eq_bot_iff_forall_leproof · cited by 1
- IsLUB.nonemptyproof · cited by 0