lt_one_add
theorem lt_one_add :
∀ {α : Type u_1} [inst : One α] [inst_1 : AddZeroClass α] [inst_2 : PartialOrder α] [inst_3 : ZeroLEOneClass α]
[inst_4 : NeZero 1] [inst_5 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1]
(a : α), a < 1 + a
The `lt_one_add` theorem states that for any type `α` that has a `One` instance, an `AddZeroClass` instance, a `PartialOrder` instance, a `ZeroLEOneClass` instance, a `NeZero 1` instance and a `CovariantClass` instance for addition and the less than relation, any element `a` of type `α` is less than the sum of `1` and `a`. This is a general property that applies to many algebraic structures such as natural numbers, integers, rational numbers, and real numbers. In mathematical terms, this theorem states that for all `a` in `α`, `a < 1 + a`.
More concisely: For any type `α` with the specified instances, every `a` in `α` satisfies `a < 1 + a`.
|
lt_add_one
theorem lt_add_one :
∀ {α : Type u_1} [inst : One α] [inst_1 : AddZeroClass α] [inst_2 : PartialOrder α] [inst_3 : ZeroLEOneClass α]
[inst_4 : NeZero 1] [inst_5 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α),
a < a + 1
This theorem, `lt_add_one`, states that for any element `a` of a certain type `α`, `a` is less than `a` plus one. The type `α` has certain properties enforced by the provided typeclasses: it has an element considered as "one" (`One α`), it supports addition with zero (`AddZeroClass α`), it has a partial order defined (`PartialOrder α`), zero is less than or equal to one (`ZeroLEOneClass α`), one is not zero (`NeZero 1`), and the addition operation is covariant, meaning that if `x < y` then `x + z < y + z` for any `z` (`CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1`).
More concisely: For any element `a` of type `α` with properties `One α`, `AddZeroClass α`, `PartialOrder α`, `ZeroLEOneClass α`, and `NeZero 1`, and covariant addition, we have `a < a + One α`.
|
zero_lt_two
theorem zero_lt_two :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [inst_2 : ZeroLEOneClass α]
[inst_3 : NeZero 1] [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], 0 < 2
This theorem, named `zero_lt_two`, states that for any type `α` that has the structures of an additive monoid with 1 (i.e., it supports addition and has a distinguished element "1"), a partial order (i.e., it supports comparison operations like ≤), and a `ZeroLEOneClass` (which enforces that 0 is less than or equal to 1), and also satisfies the properties that 1 is not zero (`NeZero 1`) and the covariant property for addition and order (`CovariantClass`), then 0 is less than 2. In other words, in a mathematical setting that supports these features, we have 0 < 2.
More concisely: If `α` is an additive monoid with 1, a partial order, and `ZeroLEOneClass` such that `1` is not zero and addition and order are covariant, then `0 < 2`.
|
three_pos
theorem three_pos :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [inst_2 : ZeroLEOneClass α]
[inst_3 : NeZero 1] [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], 0 < 3
This theorem, named `three_pos`, asserts that the number 3 is greater than 0. The theorem is applicable for any type `α` that is a monoid with additional property of having 1 as an identity element (`AddMonoidWithOne`), has a partial order (`PartialOrder`), a structure stating that 0 is less than or equal to 1 (`ZeroLEOneClass`), and a property that 1 is not zero (`NeZero 1`). Also, `α` should belong to `CovariantClass`, meaning that addition and the order relation on `α` are compatible. The theorem is an alias of the theorem `zero_lt_three`.
More concisely: The theorem `three_pos` (alias `zero_lt_three`) in Lean 4 asserts that for any type `α` being an AddMonoidWithOne, PartialOrder, ZeroLEOneClass, NeZero 1, and CovariantClass, the element 3 belongs to `α` and is greater than 0 (represented as the additive identity of `α`).
|
four_pos
theorem four_pos :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [inst_2 : ZeroLEOneClass α]
[inst_3 : NeZero 1] [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], 0 < 4
This theorem, named `four_pos`, asserts that for any type `α` that satisfies the properties of an ordered additive monoid with a distinct zero and one (i.e., it has operations of addition and a partial order, with zero less than or equal to one, and one is not zero), and the operation of addition is covariant (maintains the order), the number four is strictly greater than zero. Notice that this is an alias of `zero_lt_four` theorem and a version with explicit type is available as `zero_lt_four'`.
More concisely: For any ordered additive monoid with a distinct zero and one where addition is covariant, the number four is strictly greater than zero.
|
one_le_two
theorem one_le_two :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : LE α] [inst_2 : ZeroLEOneClass α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], 1 ≤ 2
This theorem states that, for any type `α` which is an additive monoid with a distinguished 'one' element and a 'less than or equal to' relation, and where zero is less than or equal to one, and where the addition operation is covariant (meaning that if `x ≤ y` then `x + z ≤ y + z` for all `z`), we have that one is less than or equal to two. The proof of this theorem is suppressed.
More concisely: If `α` is an additive monoid with one and a relation `≤` such that `0 ≤ 1`, `1 ≤ 2`, and addition is covariant, then `1 ≤ 2`.
|
one_lt_two
theorem one_lt_two :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [inst_2 : ZeroLEOneClass α]
[inst_3 : NeZero 1] [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1], 1 < 2
This theorem states that one is less than two in any type, `α`, which is a partially ordered monoid with a zero, a one, the property that zero is less than or equal to one, and satisfies the conditions of a non-zero one and covariant class. In other words, for any such type `α`, the number 1 is strictly less than the number 2.
More concisely: In any partially ordered monoid type `α` with a zero, a one, zero <= one, and non-zero one, the element 1 is strictly less than 2.
|
zero_lt_two'
theorem zero_lt_two' :
∀ (α : Type u_1) [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [inst_2 : ZeroLEOneClass α]
[inst_3 : NeZero 1] [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], 0 < 2
This theorem, `zero_lt_two'`, states that for any type `α` possessing certain properties (specifically, being an additive monoid with a distinguished element '1', having a partial order, satisfying the property that 0 is less than or equal to 1, that 1 is not zero, and that addition is a covariant operation), the value '0' is less than '2'. Here, '2' is likely understood as '1 + 1' in the context of the additive monoid. This theorem abstracts the common numerical fact that 0 is less than 2 into a more general setting.
More concisely: For any additive monoid with unit '1' and partial order where 0 is less than 1 and 1 is non-zero, 0 is less than 1 + 1.
|
two_pos
theorem two_pos :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [inst_2 : ZeroLEOneClass α]
[inst_3 : NeZero 1] [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], 0 < 2
This theorem, named `two_pos`, asserts that in any additive monoid with one (AddMonoidWithOne), which also has a partial order and satisfies the properties of ZeroLEOneClass, where 1 is not zero (NeZero 1) and where addition is a covariant operation, the number two is strictly greater than zero. This theorem is an alias for `zero_lt_two`. For a version where the type is made explicit, refer to `zero_lt_two'`.
More concisely: In an additive monoid with one and a partial order, where 1 is non-zero and addition is covariant, the element 2 is strictly greater than the identity element (zero).
|
zero_lt_three
theorem zero_lt_three :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [inst_2 : ZeroLEOneClass α]
[inst_3 : NeZero 1] [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], 0 < 3
This theorem, `zero_lt_three`, asserts that zero is less than three. It applies for any type `α` that satisfies several conditions: it must be an additive monoid with one, have a partial order, have a zero less than or equal to one class, not have zero as its unity (1 is not zero), and it must be a covariant class, which means that addition respects the order. In simpler terms, if you have a number system where you can add and compare numbers, and one is greater than zero, then zero is always less than three in that system.
More concisely: For any additive monoid with one and a covariant partial order where zero is less than one and one is not the unity, zero is less than three.
|
zero_lt_three'
theorem zero_lt_three' :
∀ (α : Type u_1) [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [inst_2 : ZeroLEOneClass α]
[inst_3 : NeZero 1] [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], 0 < 3
This theorem, `zero_lt_three'`, states that for any type `α` that is a `AddMonoidWithOne`, a `PartialOrder`, and a `ZeroLEOneClass`, and also satisfies the properties `NeZero 1` and `CovariantClass` for addition and ordering, the number 0 is strictly less than 3. Essentially, it is stating the mathematical property that 0 is less than 3 for any such algebraic structure that behaves like the natural numbers or integers.
More concisely: For any type `α` that is an AddMonoidWithOne, PartialOrder, ZeroLEOneClass, and satisfies NeZero 1 and CovariantClass properties for addition and ordering, 0 < 3 holds.
|
zero_lt_four'
theorem zero_lt_four' :
∀ (α : Type u_1) [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [inst_2 : ZeroLEOneClass α]
[inst_3 : NeZero 1] [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], 0 < 4
This theorem, named `zero_lt_four'`, states that for any type `α` that is an additive monoid with one, has a partial order, a zero less than or equal to one structure, a not equal to zero for one structure, and a covariant class for addition and less than or equal relation, zero is less than four.
More concisely: For any additive monoid with one and the given structures, zero is less than four.
|
zero_lt_four
theorem zero_lt_four :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [inst_2 : ZeroLEOneClass α]
[inst_3 : NeZero 1] [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], 0 < 4
This theorem, named `zero_lt_four`, states that for any type `α` with the properties of an additive monoid with unity, a partial order, a class where zero is less than or equal to one, a non-zero unity, and a covariant class under addition and order, the number zero is less than four. The proof for this theorem is not provided here. The comment suggests to look at a version of this theorem where the type is made explicit, named `zero_lt_four'`.
More concisely: For any additive monoid with unity, partial order, zero <= 1, non-zero unity, and covariant additive and order structure, zero is less than four.
|
zero_le_two
theorem zero_le_two :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : Preorder α] [inst_2 : ZeroLEOneClass α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], 0 ≤ 2
This theorem states that for any type `α` which has the structure of an additive monoid with one (namely, it has an operation of addition and a distinct element 'one', with the usual properties such as associativity and identity), a preorder (a relation that is reflexive and transitive), and a property where zero is less than or equal to one, and is a covariant class (a class where, if `x` plus some value is less than or equal to `x_1` plus some value, then `x` is less than or equal to `x_1`), then zero is less than or equal to two.
More concisely: If `α` is an additive monoid with one, has a preorder where zero is less than or equal to one, and is a covariant class, then `0 ≤ 2`.
|