Theorems · Inductive type · order theory
IsBotOneClass
(α : Type u_1) → [LE α] → [One α] → Prop
A typeclass expressing that the 1 of a type is a bottom element. In a partial OrderBot, this
is equivalent to ⊥ = 1.
- Defined in
- Mathlib.Algebra.Order.IsBotOne
- Cited by
- 35 results in Mathlib
- Foundations
- Depth 1 from the axioms · 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 by38
Results whose statement or proof uses this declaration.
- one_lestatement and proof · cited by 23
- one_lt_iff_ne_onestatement and proof · cited by 3
- IsBotOneClass.toOrderBotstatement and proof · cited by 3
- isBot_onestatement and proof · cited by 2
- one_lt_of_ne_onestatement and proof · cited by 2
- le_one_iff_eq_onestatement and proof · cited by 2
- LT.lt.one_ltstatement · cited by 2
- eq_one_of_le_onestatement and proof · cited by 1
- one_lt_of_gtstatement and proof · cited by 1
- ne_one_of_ltstatement and proof · cited by 1
- Right.one_lt_mul_of_rightstatement and proof · cited by 1
- Ne.one_ltstatement · cited by 1