Documentation

Mathlib.Algebra.Order.ZeroLEOne

Typeclass expressing 0 ≤ 1. #

source
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
    source
    @[simp]
    theorem zero_le_one {α : Type u_1} [Zero α] [One α] [LE α] [ZeroLEOneClass α] :
    0 ≤ 1

    zero_le_one with the type argument implicit.

    source
    instance ZeroLEOneClass.factZeroLeOne {α : Type u_1} [Zero α] [One α] [LE α] [ZeroLEOneClass α] :
    Fact (0 ≤ 1)
    source
    theorem zero_le_one' (α : Type u_2) [Zero α] [One α] [LE α] [ZeroLEOneClass α] :
    0 ≤ 1

    zero_le_one with the type argument explicit.

    source
    instance Prod.instZeroLEOneClass {R : Type u_2} {S : Type u_3} [Zero R] [One R] [LE R] [ZeroLEOneClass R] [Zero S] [One S] [LE S] [ZeroLEOneClass S] :
    ZeroLEOneClass (R × S)
    source
    instance Pi.instZeroLEOneClass {ι : Type u_2} {R : ι → Type u_3} [(i : ι) → Zero (R i)] [(i : ι) → One (R i)] [(i : ι) → LE (R i)] [∀ (i : ι), ZeroLEOneClass (R i)] :
    ZeroLEOneClass ((i : ι) → R i)
    source
    @[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.

    source
    instance ZeroLEOneClass.factZeroLtOne {α : Type u_1} [Zero α] [One α] [PartialOrder α] [ZeroLEOneClass α] [NeZero 1] :
    Fact (0 < 1)
    source
    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.

    source
    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.

    source
    instance Nat.instZeroLEOneClass :
    ZeroLEOneClass ℕ
    source
    instance Int.instZeroLEOneClass :
    ZeroLEOneClass Int
    source
    instance Rat.instZeroLEOneClass :
    ZeroLEOneClass Rat