Documentation

Mathlib.Algebra.Order.ZeroLEOne

Typeclass expressing 0 ≤ 1≤ 1. #

source
ink
class ZeroLEOneClass (α : Type u_1) [inst : Zero α] [inst : One α] [inst : LE α] :
Type

  • Zero is less than or equal to one.

    zero_le_one : 0 ≤ 1

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

Instances
    source
    ink
    @[simp]
    theorem zero_le_one {α : Type u_1} [inst : Zero α] [inst : One α] [inst : LE α] [inst : ZeroLEOneClass α] :
    0 ≤ 1

    zero_le_one with the type argument implicit.

    source
    ink
    theorem zero_le_one' (α : Type u_1) [inst : Zero α] [inst : One α] [inst : LE α] [inst : ZeroLEOneClass α] :
    0 ≤ 1

    zero_le_one with the type argument explicit.

    source
    ink
    @[simp]
    theorem zero_lt_one {α : Type u_1} [inst : Zero α] [inst : One α] [inst : PartialOrder α] [inst : ZeroLEOneClass α] [inst : NeZero 1] :
    0 < 1

    See zero_lt_one' for a version with the type explicit.

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

    See zero_lt_one for a version with the type implicit.

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

    Alias of zero_lt_one.