le_self_add
theorem le_self_add : ∀ {α : Type u} [inst : CanonicallyOrderedAddCommMonoid α] {a c : α}, a ≤ a + c
This theorem states that for any type `α` that forms a canonically ordered additive commutative monoid, and for any elements `a` and `c` of that type, `a` is less than or equal to the sum of `a` and `c`. In other words, in such a monoid, any element is always less than or equal to itself plus another element.
More concisely: For any additive commutative monoid with a canonical order, every element is less than or equal to the sum of itself and any other element.
|
le_of_add_le_right
theorem le_of_add_le_right : ∀ {α : Type u} [inst : CanonicallyOrderedAddCommMonoid α] {a b c : α}, a + b ≤ c → b ≤ c
This theorem, `le_of_add_le_right`, states that for any type `α` that is a canonically ordered additive commutative monoid, if the sum of two elements `a` and `b` is less than or equal to a third element `c`, then `b` is also less than or equal to `c`. The variables `a`, `b`, and `c` are all elements of the type `α`. This theorem captures an essential property of numbers where if a part (`a + b`) of something is less than or equal to the whole (`c`), then any component part (`b`) of that part is also less than or equal to the whole.
More concisely: If `a`, `b`, and `c` are elements of a commutative additive monoid `α` with a canonical order, then `a ≤ c` implies `b ≤ c`.
|
Mathlib.Algebra.Order.Monoid.Canonical.Defs._auxLemma.9
theorem Mathlib.Algebra.Order.Monoid.Canonical.Defs._auxLemma.9 :
∀ {α : Type u} [inst : CanonicallyOrderedAddCommMonoid α] {a b : α}, (a + b = 0) = (a = 0 ∧ b = 0)
This theorem states that for any given type `α`, which forms a canonically ordered additive commutative monoid, and for any two elements `a` and `b` of this type, the sum of `a` and `b` is equal to zero if and only if both `a` and `b` are zero. In other words, in the context of a canonically ordered additive commutative monoid, the only way two elements can add to zero is if both elements are zero.
More concisely: In a canonically ordered additive commutative monoid, for all elements `a` and `b`, if `a + b = 0` then both `a` and `b` are zero.
|
CanonicallyOrderedCommMonoid.le_self_mul
theorem CanonicallyOrderedCommMonoid.le_self_mul :
∀ {α : Type u_1} [self : CanonicallyOrderedCommMonoid α] (a b : α), a ≤ a * b
This theorem states that for any given two elements `a` and `b` of a canonically ordered commutative monoid `α`, `a` is less than or equal to the product of `a` and `b`. In mathematical terms, it's saying that for all `a, b` ∈ `α`, we have `a ≤ a * b`.
More concisely: For all elements `a` and `b` in a commutative monoid `α` with a canonical order, `a` is less than or equal to `a * b`.
|
NeZero.pos
theorem NeZero.pos : ∀ {M : Type u_1} (a : M) [inst : CanonicallyOrderedAddCommMonoid M] [inst_1 : NeZero a], 0 < a
The theorem `NeZero.pos` states that for any type `M` that is a canonically ordered additive commutative monoid, and for any element `a` of `M` that is not zero, `a` is strictly greater than zero. In more mathematical terms, for all `a` in `M` where `M` is a canonically ordered additive commutative monoid and `a` is not equal to zero (`a ≠ 0`), `a` is strictly greater than zero (`0 < a`).
More concisely: For any non-zero element `a` in a canonically ordered additive commutative monoid `M`, `0 < a`.
|
pos_of_gt
theorem pos_of_gt : ∀ {M : Type u_1} [inst : CanonicallyOrderedAddCommMonoid M] {n m : M}, n < m → 0 < m
This theorem states that for any type `M` that forms a canonically ordered additive commutative monoid, if `n` and `m` are elements of `M` such that `n` is less than `m`, then `m` is greater than 0. In other words, in such a monoid, any element that is greater than another element is necessarily greater than zero.
More concisely: In a canonically ordered, additive commutative monoid `M`, if `n` is less than `m` in `M`, then `m` is positive (or non-zero).
|
CanonicallyLinearOrderedAddCommMonoid.max_def
theorem CanonicallyLinearOrderedAddCommMonoid.max_def :
∀ {α : Type u_1} [self : CanonicallyLinearOrderedAddCommMonoid α] (a b : α), max a b = if a ≤ b then b else a := by
sorry
This theorem states that for any type `α` which has a structure of `CanonicallyLinearOrderedAddCommMonoid` (a canonical linear order on a commutative monoid with addition), the maximum of two elements `a` and `b` is defined as follows: if `a` is less than or equal to `b`, then `b` is the maximum; otherwise, `a` is the maximum. This definition aligns with the concept of maximum derived from the order relation `≤`.
More concisely: For any type `α` with a canonical linear order `≤` as a `CanonicallyLinearOrderedAddCommMonoid`, the maximum of two elements `a` and `b` is `a` if `a ≤ b` is false, and `b` otherwise.
|
le_of_forall_pos_le_add
theorem le_of_forall_pos_le_add :
∀ {α : Type u} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] [inst_2 : AddMonoid α] [inst_3 : ExistsAddOfLE α]
[inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_5 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α},
(∀ (ε : α), 0 < ε → a ≤ b + ε) → a ≤ b
This theorem states that for any type `α` that is a linear order, densely ordered, an additive monoid, and satisfies certain covariance and contravariance properties with respect to addition and less-than relation, given any two elements `a` and `b` of type `α`, if for every positive `ε` of type `α`, `a` is less than or equal to `b` plus `ε`, then `a` is less than or equal to `b`.
More concisely: If `α` is a linear order, densely ordered, additive monoid where `≤` is covariant with respect to addition and `≤` and `<` are contravariant with respect to addition, then for all `a`, `b` in `α`, if `a ≤ b + ε` for all positive `ε`, then `a ≤ b`.
|
CanonicallyLinearOrderedAddCommMonoid.min_def
theorem CanonicallyLinearOrderedAddCommMonoid.min_def :
∀ {α : Type u_1} [self : CanonicallyLinearOrderedAddCommMonoid α] (a b : α), min a b = if a ≤ b then a else b := by
sorry
This theorem states that for any type `α` that is an instance of `CanonicallyLinearOrderedAddCommMonoid`, the minimum function applied to any two elements `a` and `b` of `α` is equivalent to a function that checks if `a` is less than or equal to `b` and returns `a` if true, otherwise it returns `b`. In other words, the `min` function in a `CanonicallyLinearOrderedAddCommMonoid` is defined as the function `minOfLe`, which returns the smaller of two values based on the canonical linear order.
More concisely: For any `CanonicallyLinearOrderedAddCommMonoid` type `α`, the `min` function is equivalent to the function that checks if the first argument is less than or equal to the second, and returns the first argument if true, otherwise returns the second argument.
|
bot_eq_zero
theorem bot_eq_zero : ∀ {α : Type u} [inst : CanonicallyOrderedAddCommMonoid α], ⊥ = 0
This theorem states that, for any type 'α' which forms a canonically ordered additive commutative monoid, the bottom element (denoted as '⊥') is equivalent to zero. In other words, in the context of an additive commutative monoid which also respects a canonical ordering, the least element in the set is effectively the same as the additive identity, zero.
More concisely: For any additively commutative monoid with a canonical ordering, the least element equals the additive identity.
|
le_add_right
theorem le_add_right : ∀ {α : Type u} [inst : CanonicallyOrderedAddCommMonoid α] {a b c : α}, a ≤ b → a ≤ b + c := by
sorry
This theorem, `le_add_right`, states that for any type `α` that forms a canonically ordered additive commutative monoid (a mathematical structure with an operation that is both commutative and associative, an identity element, and an ordering compatible with the operation), if `a` is less than or equal to `b`, then `a` is also less than or equal to the addition of `b` and `c`. Here, `a`, `b`, and `c` are elements of `α`. This theorem is a property of ordered monoids, capturing the idea that adding something to `b` cannot decrease its value.
More concisely: For any additively commutative monoid with a canonical order, if `a` is less than or equal to `b`, then `a` is less than or equal to `b + c`.
|
CanonicallyLinearOrderedAddCommMonoid.le_total
theorem CanonicallyLinearOrderedAddCommMonoid.le_total :
∀ {α : Type u_1} [self : CanonicallyLinearOrderedAddCommMonoid α] (a b : α), a ≤ b ∨ b ≤ a
This theorem states that for any given type `α` that forms a canonically linearly ordered additive commutative monoid, for any two elements `a` and `b` of this type, either `a` is less than or equal to `b`, or `b` is less than or equal to `a`. This is essentially asserting that a linear order is total in this structure, which means that any two elements are comparable.
More concisely: For any type `α` that is a canonically linearly ordered additive commutative monoid, the relation `≤` is a total order on `α`.
|
CanonicallyLinearOrderedCommMonoid.max_def
theorem CanonicallyLinearOrderedCommMonoid.max_def :
∀ {α : Type u_1} [self : CanonicallyLinearOrderedCommMonoid α] (a b : α), max a b = if a ≤ b then b else a := by
sorry
This theorem states that, for any type `α` that forms a canonically linearly ordered commutative monoid, the maximum of two elements `a` and `b` is defined as `b` if `a` is less than or equal to `b`, otherwise it is `a`. This definition is equivalent to what you would get if you used the `maxOfLe` function.
More concisely: For any linearly ordered commutative monoid type `α`, the maximum of `a` and `b` is `a` if `a ≤ b` and `b` otherwise.
|
pos_iff_ne_zero
theorem pos_iff_ne_zero : ∀ {α : Type u} [inst : CanonicallyOrderedAddCommMonoid α] {a : α}, 0 < a ↔ a ≠ 0
This theorem, `pos_iff_ne_zero`, holds for any type `α` that is a `CanonicallyOrderedAddCommMonoid`. It asserts that for any element `a` of type `α`, `a` is greater than zero if and only if `a` is not equal to zero. In other words, in the context of a `CanonicallyOrderedAddCommMonoid`, an element is positive precisely when it is non-zero.
More concisely: In a `CanonicallyOrderedAddCommMonoid`, an element is positive if and only if it is non-zero.
|
CanonicallyOrderedCommMonoid.exists_mul_of_le
theorem CanonicallyOrderedCommMonoid.exists_mul_of_le :
∀ {α : Type u_1} [self : CanonicallyOrderedCommMonoid α] {a b : α}, a ≤ b → ∃ c, b = a * c
This theorem states that for any given type 'α', which is a Canonically Ordered Commutative Monoid, if 'a' and 'b' are elements of this type such that 'a' is less than or equal to 'b', then there exists an element 'c' in the same type such that 'b' is equal to the product of 'a' and 'c'. Essentially, if 'a' is less than or equal to 'b', then 'b' can be expressed as a multiple of 'a'.
More concisely: For any Canonically Ordered Commutative Monoid type 'α' and elements 'a' and 'b' with 'a' <= 'b', there exists 'c' in 'α' such that 'b' = 'a' * 'c'.
|
bot_eq_zero'
theorem bot_eq_zero' : ∀ {α : Type u} [inst : CanonicallyLinearOrderedAddCommMonoid α], ⊥ = 0
This theorem states that in any canonically linearly ordered additive commutative monoid, the bottom element is equal to zero. In other words, for any type `α` that has a structure of a canonically linearly ordered additive commutative monoid, the lowest possible value or the smallest element (`⊥`) is always zero (`0`).
More concisely: In any canonically linearly ordered additive commutative monoid, the least element is equal to zero.
|
le_iff_exists_mul
theorem le_iff_exists_mul : ∀ {α : Type u} [inst : CanonicallyOrderedCommMonoid α] {a b : α}, a ≤ b ↔ ∃ c, b = a * c
This theorem states that for any canonically ordered commutative monoid `α`, and any elements `a` and `b` of `α`, `a` is less than or equal to `b` if and only if there exists an element `c` in `α` such that `b` equals `a` multiplied by `c`. In other words, in this type of monoid, an element `a` is not greater than another element `b` exactly when `b` is a multiple of `a`.
More concisely: For any commutative monoid equipped with a canonical order, element `a` is less than or equal to `b` if and only if `b` is a multiple of `a`.
|
nonpos_iff_eq_zero
theorem nonpos_iff_eq_zero : ∀ {α : Type u} [inst : CanonicallyOrderedAddCommMonoid α] {a : α}, a ≤ 0 ↔ a = 0 := by
sorry
This theorem, `nonpos_iff_eq_zero`, states that for any type `α` that is a canonically ordered additive commutative monoid, an element `a` of type `α` is non-positive (i.e., `a ≤ 0`) if and only if `a` is equal to zero (`a = 0`). In other words, in such a data structure, the only non-positive element is zero itself.
More concisely: For any additive commutative monoid `α` with canonical order, an element `a` in `α` is non-positive if and only if it is equal to zero.
|
le_mul_self
theorem le_mul_self : ∀ {α : Type u} [inst : CanonicallyOrderedCommMonoid α] {a b : α}, a ≤ b * a
This theorem, `le_mul_self`, states that for any type `α` that is a canonically ordered commutative monoid, for any elements `a` and `b` of this type, `a` is less than or equal to the product of `b` and `a`. In other words, in a canonically ordered commutative monoid, multiplication by any element doesn't decrease the value of the original element.
More concisely: In a commutative monoid endowed with a canonical order, for all elements `a` and `b`, we have `a <= b * a`.
|
one_le
theorem one_le : ∀ {α : Type u} [inst : CanonicallyOrderedCommMonoid α] (a : α), 1 ≤ a
This theorem states that for any type `α` that is a Canonically Ordered Commutative Monoid, any element `a` of this type `α` is greater than or equal to 1. In other words, in a canonically ordered commutative monoid, no element can be less than the identity element 1.
More concisely: In a canonically ordered commutative monoid, every element is greater than or equal to the identity element 1.
|
zero_min
theorem zero_min : ∀ {α : Type u} [inst : CanonicallyLinearOrderedAddCommMonoid α] (a : α), min 0 a = 0
This theorem states that for all types `α` that form a "Canonically Linear Ordered Additive Commutative Monoid", the minimum of `0` and any element `a` of type `α` is always `0`. In mathematical terms, given any canonically linearly ordered additive commutative monoid (which is a structure that combines properties of an ordered set, a commutative group, and a monoid), this theorem asserts the property that zero is less than or equal to any element of the set, or equivalently, for any element `a`, `min(0, a) = 0`.
More concisely: In any canonically linearly ordered additive commutative monoid, the minimum element is 0.
|
ExistsAddOfLE.exists_add_of_le
theorem ExistsAddOfLE.exists_add_of_le :
∀ {α : Type u} [inst : Add α] [inst_1 : LE α] [self : ExistsAddOfLE α] {a b : α}, a ≤ b → ∃ c, b = a + c
The theorem, `exists_add_of_le`, states that for any type `α` that supports addition and comparison, given `a` and `b` of type `α` where `a` is less than or equal to `b`, there exists a `c` of type `α` such that `b` is equal to `a` plus `c`.
More concisely: For all types `α` with add and order structures, if `a` is an element of `α` less than or equal to `b`, then there exists an element `c` in `α` such that `b = a + c`.
|
bot_eq_one'
theorem bot_eq_one' : ∀ {α : Type u} [inst : CanonicallyLinearOrderedCommMonoid α], ⊥ = 1
This theorem states that in any canonically linearly ordered commutative monoid, the bottom element is equal to the identity element. In other words, for all types `α` that have a `CanonicallyLinearOrderedCommMonoid` structure, the least element in the set (`⊥`) is the same as the multiplicative identity (`1`).
More concisely: In any commutative monoid endowed with a canonical linear order, the least element is the multiplicative identity.
|
CanonicallyLinearOrderedCommMonoid.le_total
theorem CanonicallyLinearOrderedCommMonoid.le_total :
∀ {α : Type u_1} [self : CanonicallyLinearOrderedCommMonoid α] (a b : α), a ≤ b ∨ b ≤ a
This theorem states that for any type `α` which is a canonically linearly ordered commutative monoid, and for any elements `a` and `b` of this type, either `a` is less than or equal to `b` or `b` is less than or equal to `a`. In other words, it asserts the property of total ordering for the given type, meaning every pair of elements is comparable.
More concisely: For any type `α` that is both a canonically linearly ordered and commutative monoid, its elements `a` and `b` satisfy `a ≤ b` or `b ≤ a`.
|
CanonicallyLinearOrderedCommMonoid.min_def
theorem CanonicallyLinearOrderedCommMonoid.min_def :
∀ {α : Type u_1} [self : CanonicallyLinearOrderedCommMonoid α] (a b : α), min a b = if a ≤ b then a else b := by
sorry
This theorem states that for any type `α` which is a canonically linearly ordered commutative monoid, the minimum between two elements `a` and `b` of this type is defined as `a` if `a` is less than or equal to `b`, otherwise it is `b`. In simpler terms, this theorem defines the `min` function in terms of the `≤` (less than or equal to) relation.
More concisely: For any canonically linearly ordered commutative monoid type `α`, the minimum of two elements `a` and `b` is `a` if `a` is less than or equal to `b`, and `b` otherwise. (i.e., `min a b = if h : a ≤ b then a else b`)
|
add_eq_zero_iff
theorem add_eq_zero_iff :
∀ {α : Type u} [inst : CanonicallyOrderedAddCommMonoid α] {a b : α}, a + b = 0 ↔ a = 0 ∧ b = 0
This theorem states that for any given type `α` which is a canonically ordered additive commutative monoid, the sum of two elements `a` and `b` is equal to zero if and only if both `a` and `b` are equal to zero. In other words, in this type of monoid, the only way for the sum of two elements to be zero is if both elements are zero themselves. This theorem is a key property of all canonically ordered additive commutative monoids.
More concisely: In a canonically ordered additive commutative monoid, the sum of two elements is zero if and only if both elements are zero.
|
le_iff_exists_add
theorem le_iff_exists_add :
∀ {α : Type u} [inst : CanonicallyOrderedAddCommMonoid α] {a b : α}, a ≤ b ↔ ∃ c, b = a + c
This theorem, `le_iff_exists_add`, states that for any type `α` that is a canonically ordered additive commutative monoid, for any two elements `a` and `b` of `α`, `a` is less than or equal to `b` if and only if there exists a third element `c` such that `b` equals `a` plus `c`. Essentially, this theorem provides a way to express the order relation (`≤`) in terms of the addition operation in the monoid.
More concisely: For any additive commutative monoid with a canonical order, element `a` is less than or equal to element `b` if and only if `b` is the sum of `a` and some element `c`.
|
CanonicallyLinearOrderedAddCommMonoid.compare_eq_compareOfLessAndEq
theorem CanonicallyLinearOrderedAddCommMonoid.compare_eq_compareOfLessAndEq :
∀ {α : Type u_1} [self : CanonicallyLinearOrderedAddCommMonoid α] (a b : α), compare a b = compareOfLessAndEq a b
This theorem states that for any type `α`, which is equipped with a `CanonicallyLinearOrderedAddCommMonoid` structure, the `compare` function on elements `a` and `b` of type `α` is equal to the `compareOfLessAndEq` function on the same elements `a` and `b`. In other words, the ordering determined by the `compare` function is equivalent to the ordering determined by the `compareOfLessAndEq` function, given that `<` and `=` are decidable (that is, there is a concrete way to determine whether `a` is less than `b`, or `a` is equal to `b`).
More concisely: For any type `α` with a `CanonicallyLinearOrderedAddCommMonoid` structure, the `compare` and `compareOfLessAndEq` functions on `α` agree when `<` and `=` are decidable.
|
Mathlib.Algebra.Order.Monoid.Canonical.Defs._auxLemma.7
theorem Mathlib.Algebra.Order.Monoid.Canonical.Defs._auxLemma.7 :
∀ {α : Type u} [inst : CanonicallyOrderedAddCommMonoid α] (a : α), (0 ≤ a) = True
This theorem, in the context of a canonically ordered additive commutative monoid, states that zero is less than or equal to any element of the monoid. In more specific terms, for any type `α` that forms a canonically ordered additive commutative monoid, and for any element `a` of this type, it asserts the truth of the inequality `0 ≤ a`.
More concisely: In a canonically ordered additive commutative monoid, the zero element is less than or equal to every other element.
|
le_of_forall_one_lt_le_mul
theorem le_of_forall_one_lt_le_mul :
∀ {α : Type u} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] [inst_2 : Monoid α] [inst_3 : ExistsMulOfLE α]
[inst_4 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
[inst_5 : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b : α},
(∀ (ε : α), 1 < ε → a ≤ b * ε) → a ≤ b
This theorem states that for any type `α` that has a linear order, is densely ordered, has a monoid structure, has a multiplication associated with less than or equal to, and has two types of covariance on multiplication and less than, if for all `ε` out of `α` that are greater than 1 it holds that `a` is less than or equal to `b * ε`, then `a` is less than or equal to `b`.
More concisely: If `α` is a type with a dense linear order, a monoid structure, and covariance on multiplication and order such that for all `ε > 1` in `α`, we have `a ≤ b * ε`, then `a ≤ b`.
|
CanonicallyLinearOrderedCommMonoid.compare_eq_compareOfLessAndEq
theorem CanonicallyLinearOrderedCommMonoid.compare_eq_compareOfLessAndEq :
∀ {α : Type u_1} [self : CanonicallyLinearOrderedCommMonoid α] (a b : α), compare a b = compareOfLessAndEq a b := by
sorry
This theorem states that for any canonically linear ordered commutative monoid `α` and any two elements `a` and `b` of `α`, the comparison of `a` and `b` using the `compare` function is equal to the comparison of `a` and `b` using the `compareOfLessAndEq` function. The `compare` function is the canonical way of comparing elements in the monoid, and the `compareOfLessAndEq` function is defined in terms of the less-than `<` and equality `=` comparisons, which are decidable (i.e., there exists a procedure that can definitively say whether `a` is less than, equal to, or greater than `b`).
More concisely: For any commutative monoid endowed with a canonical linear order, the comparison function `compare` and the comparison function `compareOfLessAndEq` based on less-than and equality comparisons agree.
|
le_add_left
theorem le_add_left : ∀ {α : Type u} [inst : CanonicallyOrderedAddCommMonoid α] {a b c : α}, a ≤ c → a ≤ b + c := by
sorry
This theorem, named `le_add_left`, states that for any type `α` that forms a canonically ordered additive commutative monoid, given three elements `a`, `b` and `c` of this type, if `a` is less than or equal to `c` (`a ≤ c`), then `a` is also less than or equal to the sum of `b` and `c` (`a ≤ b + c`). This theorem provides a property about the relation between elements of a canonically ordered additive commutative monoid.
More concisely: For any additive commutative monoid with a canonical order, if `a` is less than or equal to `c`, then `a` is also less than or equal to `c + b`.
|
le_add_self
theorem le_add_self : ∀ {α : Type u} [inst : CanonicallyOrderedAddCommMonoid α] {a b : α}, a ≤ b + a
This theorem states that for any type `α` that forms a canonically ordered additive commutative monoid, and for any two elements `a` and `b` of that type, `a` is less than or equal to the sum of `b` and `a`. Here, the `CanonicallyOrderedAddCommMonoid` is a specific structure in mathematics that combines the properties of an additive commutative monoid (where addition is associative and commutative, and there's a "zero" element that doesn't change other elements when added) with a canonical order (a way of comparing elements).
More concisely: For any type `α` with a canonical order and the structure of an additive commutative monoid, `a ≤ a + b` for all `a, b : α`.
|
self_le_add_right
theorem self_le_add_right : ∀ {α : Type u} [inst : CanonicallyOrderedAddCommMonoid α] (a b : α), a ≤ a + b
This theorem states that for any type `α` that is a canonically ordered additive commutative monoid, and for any two elements `a` and `b` of this type, `a` is less than or equal to the sum of `a` and `b`. In simpler terms, for any two numbers `a` and `b` in a certain kind of ordered number system, adding `b` to `a` will not make the total smaller than `a`.
More concisely: For any additive commutative monoid with a canonical order `α`, for all `a, b ∈ α`, we have `a ≤ a + b`.
|
Mathlib.Algebra.Order.Monoid.Canonical.Defs._auxLemma.11
theorem Mathlib.Algebra.Order.Monoid.Canonical.Defs._auxLemma.11 :
∀ {α : Type u} [inst : CanonicallyOrderedAddCommMonoid α] {a : α}, (a ≤ 0) = (a = 0)
This theorem, from the `Mathlib.Algebra.Order.Monoid.Canonical.Defs` namespace, asserts that for any type `α` that is a canonically ordered additive commutative monoid, any element `a` of this type is less than or equal to 0 if, and only if, `a` is equal to 0.
More concisely: For any additive commutative monoid with a canonical order, an element is less than or equal to 0 if and only if it is equal to 0.
|
zero_le
theorem zero_le : ∀ {α : Type u} [inst : CanonicallyOrderedAddCommMonoid α] (a : α), 0 ≤ a
This theorem declares that for every instance `a` of a type `α`, where `α` is a Canonically Ordered Additive Commutative Monoid, the value `0` is less than or equal to `a`. In simpler terms, it is stating that zero is always less than or equal to any element in a given canonically ordered additive commutative monoid. This aligns with our intuitive understanding of numbers where zero is the smallest number in the set of non-negative numbers.
More concisely: For every element `a` in a canonically ordered, additive commutative monoid `α`, we have `0 ≤ a`.
|
CanonicallyOrderedAddCommMonoid.le_self_add
theorem CanonicallyOrderedAddCommMonoid.le_self_add :
∀ {α : Type u_1} [self : CanonicallyOrderedAddCommMonoid α] (a b : α), a ≤ a + b
This theorem states that for any type `α`, which is an instance of a `CanonicallyOrderedAddCommMonoid`, and any two elements `a` and `b` of this type, `a` is always less than or equal to the sum of `a` and `b`. A `CanonicallyOrderedAddCommMonoid` is a type that has both additive commutative monoid and canonical order properties, where the addition operation is commutative and the order satisfies several canonical properties.
More concisely: For any `CanonicallyOrderedAddCommMonoid` type `α` and elements `a, b` of `α`, `a ≤ a + b`.
|
le_self_mul
theorem le_self_mul : ∀ {α : Type u} [inst : CanonicallyOrderedCommMonoid α] {a c : α}, a ≤ a * c
This theorem states that for any type `α` which is a canonically ordered commutative monoid, and any elements `a` and `c` of `α`, `a` is less than or equal to the product of `a` and `c`. This is a property of the multiplicative structure in canonically ordered commutative monoids.
More concisely: In a canonically ordered commutative monoid `α`, for all elements `a` and `c` in `α`, we have `a ≤ a * c`.
|
ExistsMulOfLE.exists_mul_of_le
theorem ExistsMulOfLE.exists_mul_of_le :
∀ {α : Type u} [inst : Mul α] [inst_1 : LE α] [self : ExistsMulOfLE α] {a b : α}, a ≤ b → ∃ c, b = a * c
This theorem asserts that for any two elements `a` and `b` of a type `α` that supports multiplication and a less-than-or-equal-to relation, if `a` is less than or equal to `b`, then there exists an element `c` such that `b` is equal to the product of `a` and `c`. This essentially means `a` left divides `b`. This theorem holds in any context where `ExistsMulOfLE α` is true, which means there necessarily exists such a `c` whenever `a` is less than or equal to `b`.
More concisely: Given type `α` with multiplication and a least-than-or-equal-to relation, for any `a` less than or equal to `b` in `α`, there exists `c` such that `b = a * c`.
|
Mathlib.Algebra.Order.Monoid.Canonical.Defs._auxLemma.15
theorem Mathlib.Algebra.Order.Monoid.Canonical.Defs._auxLemma.15 :
∀ {α : Type u} [inst : CanonicallyOrderedAddCommMonoid α] {a b : α}, (0 < a + b) = (0 < a ∨ 0 < b)
This theorem from the Mathlib library in the Algebra.Order.Monoid.Canonical.Defs module is named '_auxLemma.15'. It states that for any type `α` that forms a 'CanonicallyOrderedAddCommMonoid', and for any two elements `a` and `b` of that type, the statement that `0` is less than the sum of `a` and `b` is equivalent to the statement that `0` is less than `a` or `0` is less than `b`. This theorem holds true under the mathematical rules of 'CanonicallyOrderedAddCommMonoid' and applies to any element from such a set.
More concisely: For any CanonicallyOrderedAddCommMonoid type `α` and elements `a`, `b` in `α`, `0` is less than `a + b` if and only if `0` is less than `a` or `0` is less than `b`.
|
CanonicallyOrderedAddCommMonoid.exists_add_of_le
theorem CanonicallyOrderedAddCommMonoid.exists_add_of_le :
∀ {α : Type u_1} [self : CanonicallyOrderedAddCommMonoid α] {a b : α}, a ≤ b → ∃ c, b = a + c
This theorem states that for any canonically ordered additive commutative monoid, given that `a` is less than or equal to `b`, there exists a `c` such that `b` can be expressed as the sum of `a` and `c`. A canonically ordered additive commutative monoid is a structure that satisfies the properties of being an additive commutative monoid (where addition is associative, commutative, and there is an additive identity) with a total order that is compatible with the operation, and every element is greater than or equal to the identity element.
More concisely: In a canonically ordered additive commutative monoid, for every `a` less than or equal to `b`, there exists `c` such that `b = a + c`.
|
self_le_add_left
theorem self_le_add_left : ∀ {α : Type u} [inst : CanonicallyOrderedAddCommMonoid α] (a b : α), a ≤ b + a
This theorem, `self_le_add_left`, states that for any canonically ordered additive commutative monoid `α`, and for any two elements `a` and `b` from `α`, `a` is less than or equal to the sum of `b` and `a`. In other words, for any two elements in a commutative monoid that follows a canonical order, the value of any element is always less than or equal to the sum of this element and any other element from the same monoid.
More concisely: For any commutative additive monoid `α` and its elements `a` and `b`, `a ≤ b + a`.
|