Mathlib.Algebra.Order.ZeroLEOne._auxLemma.2
theorem Mathlib.Algebra.Order.ZeroLEOne._auxLemma.2 :
∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : PartialOrder α] [inst_3 : ZeroLEOneClass α]
[inst_4 : NeZero 1], (0 < 1) = True
This theorem, named `_auxLemma.2` in the `Mathlib.Algebra.Order.ZeroLEOne` namespace, asserts that for any type `α` with instances of `Zero α`, `One α`, `PartialOrder α`, `ZeroLEOneClass α`, and `NeZero 1`, the statement "0 is less than 1" is true. This is essentially a formalization of the basic mathematical fact that 0 is less than 1, and it applies to any type that has a zero, a one, a partial order, satisfies the `ZeroLEOneClass`, and where 1 is not zero.
More concisely: For any type with a zero, one, a partial order, and `ZeroLEOneClass` structure where one is non-zero, zero is less than one.
|
zero_le_one'
theorem zero_le_one' :
∀ (α : Type u_2) [inst : Zero α] [inst_1 : One α] [inst_2 : LE α] [inst_3 : ZeroLEOneClass α], 0 ≤ 1
The theorem `zero_le_one'` states that for any type `α` that has zero, one, and a less than or equal to operation defined, and additionally satisfies the condition of the `ZeroLEOneClass` (which requires that zero is less than or equal to one), the statement that zero is less than or equal to one is always true.
More concisely: For any type `α` with zero, one, and a `<=` operation satisfying `ZeroLEOneClass`, we have `0 <= 1`.
|
zero_lt_one'
theorem zero_lt_one' :
∀ (α : Type u_1) [inst : Zero α] [inst_1 : One α] [inst_2 : PartialOrder α] [inst_3 : ZeroLEOneClass α]
[inst_4 : NeZero 1], 0 < 1
This theorem, `zero_lt_one'`, states that for any type `α` which has the operations of zero and one defined, and also has a partial order and a `ZeroLEOneClass`, which asserts that zero is less than or equal to one, we always have that zero is strictly less than one, given an additional constraint that one is not equal to zero.
More concisely: For any type with zero, one, a partial order, and `ZeroLEOneClass` where one is non-zero, zero is strictly less than one.
|
Mathlib.Algebra.Order.ZeroLEOne._auxLemma.1
theorem Mathlib.Algebra.Order.ZeroLEOne._auxLemma.1 :
∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : LE α] [inst_3 : ZeroLEOneClass α], (0 ≤ 1) = True := by
sorry
This theorem, named `Mathlib.Algebra.Order.ZeroLEOne._auxLemma.1`, states that for any type `α` which is equipped with a zero element, a one element, a less than or equal to (`LE`) operation, and belongs to the `ZeroLEOneClass` (which requires that zero is less than or equal to one in the type), the proposition that zero is less than or equal to one (`0 ≤ 1`) is always true. Essentially, this theorem formalizes the common mathematical understanding that 0 is less than or equal to 1.
More concisely: For any type with a zero, one, and the `ZeroLEOne` structure, zero is less than or equal to one.
|
ZeroLEOneClass.zero_le_one
theorem ZeroLEOneClass.zero_le_one :
∀ {α : Type u_2} [inst : Zero α] [inst_1 : One α] [inst_2 : LE α] [self : ZeroLEOneClass α], 0 ≤ 1
The theorem `ZeroLEOneClass.zero_le_one` states that for any type `α`, given that `α` has a zero element, a one element, and a less than or equal to operation defined on it, and is of the class `ZeroLEOneClass`, the number zero is less than or equal to the number one. This is a foundational theorem, applicable in any numerical system where we have defined zero, one and a less than or equal to relation.
More concisely: For any type `α` in `ZeroLEOneClass`, its zero element is less than or equal to its one element.
|
zero_le_one
theorem zero_le_one :
∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : LE α] [inst_3 : ZeroLEOneClass α], 0 ≤ 1
The theorem `zero_le_one` asserts that for any type `α` which has definitions for zero and one and an order relation (`LE`), and for which zero is less than or equal to one (`ZeroLEOneClass`), the value zero is always less than or equal to the value one.
More concisely: For any type with zero, one, and a total order where zero is less than or equal to one, zero is less than or equal to one.
|
one_pos
theorem one_pos :
∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : PartialOrder α] [inst_3 : ZeroLEOneClass α]
[inst_4 : NeZero 1], 0 < 1
The theorem `one_pos` states that, for any type `α` that has zero and one elements, and is a partial order where zero is less than or equal to one, and one is not zero, then zero is strictly less than one. This is an alias of the theorem `zero_lt_one`. See `zero_lt_one'` for a version with the type explicit.
More concisely: If `α` is a type with zero and one, is a partial order where zero is less than or equal to one, and one is not zero, then zero is strictly less than one.
|
zero_lt_one
theorem zero_lt_one :
∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : PartialOrder α] [inst_3 : ZeroLEOneClass α]
[inst_4 : NeZero 1], 0 < 1
This theorem states that for any type `α` that has zero and one as elements, along with a partial order and is a `ZeroLEOneClass` where zero is less than or equal to one, and where one is not zero, zero is strictly less than one. Essentially, it's asserting the mathematical truism that 0 < 1 under general conditions.
More concisely: For any type `α` with zero and one as elements, having a partial order and being a `ZeroLEOneClass` with zero less than one, we have 0 < 1.
|