Typeclass expressing 0 ≤ 1≤ 1
. #
@[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.
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.
@[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.
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.
theorem
one_pos
{α : Type u_1}
[inst : Zero α]
[inst : One α]
[inst : PartialOrder α]
[inst : ZeroLEOneClass α]
[inst : NeZero 1]
:
0 < 1
Alias of zero_lt_one
.