Mathlib.Algebra.Order.ZeroLEOne

ZeroLEOneClass structure

(α : Type*) [Zero α] [One α] [LE α]

Full source

/-- Typeclass for expressing that the `0` of a type is less or equal to its `1`. -/
class ZeroLEOneClass (α : Type*) [Zero α] [One α] [LE α] : Prop where
  /-- Zero is less than or equal to one. -/
  zero_le_one : (0 : α) ≤ 1

Zero less than or equal to one typeclass

Informal description

A typeclass expressing that in a type $\alpha$ equipped with a zero element $0$, a one element $1$, and a less-or-equal relation $\leq$, the inequality $0 \leq 1$ holds.

zero_le_one theorem

[Zero α] [One α] [LE α] [ZeroLEOneClass α] : (0 : α) ≤ 1

Full source

/-- `zero_le_one` with the type argument implicit. -/
@[simp] lemma zero_le_one [Zero α] [One α] [LE α] [ZeroLEOneClass α] : (0 : α) ≤ 1 :=
  ZeroLEOneClass.zero_le_one

Zero is less than or equal to one in ordered structures

Informal description

For any type $\alpha$ equipped with a zero element $0$, a one element $1$, a less-or-equal relation $\leq$, and satisfying the `ZeroLEOneClass` condition, we have $0 \leq 1$.

zero_le_one' theorem

(α) [Zero α] [One α] [LE α] [ZeroLEOneClass α] : (0 : α) ≤ 1

Full source

/-- `zero_le_one` with the type argument explicit. -/
lemma zero_le_one' (α) [Zero α] [One α] [LE α] [ZeroLEOneClass α] : (0 : α) ≤ 1 :=
  zero_le_one

Zero is less than or equal to one in ordered structures

Informal description

For any type $\alpha$ equipped with a zero element $0$, a one element $1$, a less-or-equal relation $\leq$, and satisfying the `ZeroLEOneClass` condition, we have $0 \leq 1$.

zero_lt_one theorem

: (0 : α) < 1

Full source

/-- See `zero_lt_one'` for a version with the type explicit. -/
@[simp] lemma zero_lt_one : (0 : α) < 1 := zero_le_one.lt_of_ne (NeZero.ne' 1)

Strict inequality: $0 < 1$ in ordered structures

Informal description

For any type $\alpha$ equipped with a zero element $0$, a one element $1$, and a strict order relation $<$, the inequality $0 < 1$ holds.

zero_lt_one' theorem

: (0 : α) < 1

Full source

/-- See `zero_lt_one` for a version with the type implicit. -/
lemma zero_lt_one' : (0 : α) < 1 := zero_lt_one

Strict inequality: $0 < 1$ in ordered structures

Informal description

For any type $\alpha$ equipped with a zero element $0$, a one element $1$, and a strict order relation $<$, the inequality $0 < 1$ holds.