Typeclass expressing 0 ≤ 1.

class ZeroLEOneClass (α : Type u_2) [Zero α] [One α] [LE α] : Prop

Typeclass for expressing that the 0 of a type is less or equal to its 1.

• zero_le_one : 0 ≤ 1

  Zero is less than or equal to one.

Instances

• LinearOrderedCommMonoidWithZero.toZeroLeOneClass
• OrderedSemiring.zeroLEOneClass
• WithBot.zeroLEOneClass
• WithTop.zeroLEOneClass
• canonicallyOrderedAddCommMonoid.toZeroLeOneClass

theorem ZeroLEOneClass.zero_le_one {α : Type u_2} [Zero α] [One α] [LE α] [self : ZeroLEOneClass α] : 0 ≤ 1

Zero is less than or equal to one.

@[simp]

theorem zero_le_one {α : Type u_1} [Zero α] [One α] [LE α] [ZeroLEOneClass α] : 0 ≤ 1

zero_le_one with the type argument implicit.

theorem zero_le_one' (α : Type u_2) [Zero α] [One α] [LE α] [ZeroLEOneClass α] : 0 ≤ 1

zero_le_one with the type argument explicit.

@[simp]

theorem zero_lt_one {α : Type u_1} [Zero α] [One α] [PartialOrder α] [ZeroLEOneClass α] [NeZero 1] : 0 < 1

See zero_lt_one' for a version with the type explicit.

theorem zero_lt_one' (α : Type u_1) [Zero α] [One α] [PartialOrder α] [ZeroLEOneClass α] [NeZero 1] : 0 < 1

See zero_lt_one for a version with the type implicit.

theorem one_pos {α : Type u_1} [Zero α] [One α] [PartialOrder α] [ZeroLEOneClass α] [NeZero 1] : 0 < 1

Alias of zero_lt_one.

---

See zero_lt_one' for a version with the type explicit.