Structures · Algebra
IsBotOneClass
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
- Shape
- One type argument · adds isBot_one
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- PNat
- Associates
- WithTop
How is a type an instance?
Loading the hierarchy index…
Assumed by38
- one_le
- one_lt_iff_ne_one
- IsBotOneClass.toOrderBot
- LT.lt.one_lt
- isBot_one
- le_one_iff_eq_one
- one_lt_of_ne_one
- Right.one_lt_mul_of_right
- Left.one_lt_mul_of_left
- one_lt_of_gt
- eq_one_of_le_one
- Ne.one_lt
- bot_eq_one
- ne_one_of_lt
- IsBotOneClass.isBot_one
- not_lt_one
- WithTop.instIsBotOneClass
- Set.Iio_one_eq_empty
- NE.ne.one_lt
- Finset.Ici_one_eq_univ
- Left.one_lt_mul_of_right
- one_max
- one_lt_mul_of_right
- Set.Ici_one_eq_univ
- max_one
- eq_one_or_one_lt
- LE.le.eq_one
- one_notMem_iff
- Right.one_lt_mul_of_left
- max_eq_one
- one_min
- Finset.sup'_eq_one
- min_one
- Finset.sup_eq_one
- min_eq_one
- LT.lt.ne_one
- one_lt_mul_of_left
- Set.isEmpty_Iio_one
Ancestors0
No ancestors.