mathlib3 documentation

algebra.order.zero_le_one

Typeclass expressing 0 ≤ 1. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[class]
structure zero_le_one_class (α : Type u_2) [has_zero α] [has_one α] [has_le α] :
Type
  • zero_le_one : 0 ≤ 1

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

Instances of this typeclass
Instances of other typeclasses for zero_le_one_class
  • zero_le_one_class.has_sizeof_inst
source
@[simp]
theorem zero_le_one {α : Type u_1} [has_zero α] [has_one α] [has_le α] [zero_le_one_class α] :
0 ≤ 1

zero_le_one with the type argument implicit.

source
theorem zero_le_one' (α : Type u_1) [has_zero α] [has_one α] [has_le α] [zero_le_one_class α] :
0 ≤ 1

zero_le_one with the type argument explicit.

source
@[simp]
theorem zero_lt_one {α : Type u_1} [has_zero α] [has_one α] [partial_order α] [zero_le_one_class α] [ne_zero 1] :
0 < 1

See zero_lt_one' for a version with the type explicit.

source
theorem zero_lt_one' (α : Type u_1) [has_zero α] [has_one α] [partial_order α] [zero_le_one_class α] [ne_zero 1] :
0 < 1

See zero_lt_one for a version with the type implicit.

source
theorem one_pos {α : Type u_1} [has_zero α] [has_one α] [partial_order α] [zero_le_one_class α] [ne_zero 1] :
0 < 1

Alias of zero_lt_one.