one_lt_pow'
theorem one_lt_pow' :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : M},
1 < a → ∀ {k : ℕ}, k ≠ 0 → 1 < a ^ k
This theorem states that for any type `M` with a monoid structure and a preorder, and it is a Covariant Class with respect to multiplication and the given preorder, then for any element `a` of `M`, if `a` is greater than one, for any natural number `k` not equal to zero, `a` raised to the power of `k` is also greater than one. This is essentially a property of exponents in ordered monoids, asserting that any number greater than one remains greater than one when raised to a non-zero power.
More concisely: For any covariant monoid `M` with a preorder, if `a` is an element of `M` greater than one, then `a^k` is also greater than one for any non-zero natural number `k`.
|
Monotone.pow_right
theorem Monotone.pow_right :
∀ {β : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [inst_2 : Preorder β]
[inst_3 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {f : β → M},
Monotone f → ∀ (n : ℕ), Monotone fun a => f a ^ n
This theorem, known as `Monotone.pow_right`, states that for any given types `β` and `M`, where `M` is a monoid and both `M` and `β` are preordered. Furthermore, if `M` is both left and right covariant, meaning that for all elements `x` and `x_1` in `M`, multiplying `x` and `x_1` respects the preorder relation, then for any function `f` from `β` to `M` that is monotone (meaning that if `a ≤ b` then `f(a) ≤ f(b)`), for any natural number `n`, the function that maps `a` in `β` to the `n`-th power of `f(a)` in `M` is also monotone.
More concisely: If `M` is a monoid preordered like `β`, and both `M` and `β` are covariant, then any monotone function from `β` to `M` maps increasing elements to increasing powers.
|
zsmul_nonneg
theorem zsmul_nonneg :
∀ {G : Type u_2} [inst : SubNegMonoid G] [inst_1 : Preorder G]
[inst_2 : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {x : G},
0 ≤ x → ∀ {n : ℤ}, 0 ≤ n → 0 ≤ n • x
This theorem, `zsmul_nonneg`, asserts that for any type `G` that has a subtraction and negation operation (i.e., it's a `SubNegMonoid`), is ordered (i.e., it's a `Preorder`), and satisfies a certain covariance property, if `x` is a non-negative element of `G`, then the result of scaling `x` by any non-negative integer `n` (denoted `n • x`) is also non-negative. In other words, scaling a non-negative number by a non-negative integer will yield a non-negative result in an ordered subtraction-negation monoid.
More concisely: If `G` is a subtraction-negation monoid that is ordered and satisfies the covariance property, then for all non-negative integers `n` and non-negative elements `x` of `G`, `n • x` is also non-negative.
|
lt_of_pow_lt_pow'
theorem lt_of_pow_lt_pow' :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M]
[inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : M} (n : ℕ),
a ^ n < b ^ n → a < b
This theorem, which is an alias of `lt_of_pow_lt_pow_left'`, states that for any type `M` equipped with a monoid structure, a linear order, and two covariant classes - one for multiplication `*` and the other for the swapped version of multiplication, if `a` and `b` are elements of `M` and `n` is a natural number such that `a` to the power `n` is less than `b` to the power `n`, then `a` is less than `b`.
More concisely: If `a` is less than `b` in the monoid `M` equipped with a linear order, and `a^n` (the `n`th power of `a`) is less than `b^n` for some natural number `n`, then `a` is less than `b`.
|
one_le_pow_of_one_le'
theorem one_le_pow_of_one_le' :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : M}, 1 ≤ a → ∀ (n : ℕ), 1 ≤ a ^ n
This theorem states that for any type `M` that is a monoid and has a preorder, and where the multiplication operation is covariant in the sense that if `x ≤ y` then `x * z ≤ y * z` for all `z`, if `1 ≤ a` for some `a` of type `M`, then `1 ≤ a^n` for all natural numbers `n`. In other words, if a value `a` is greater than or equal to one in a preordered monoid, then its power `n` is also greater than or equal to one for any natural number `n`.
More concisely: In a preordered monoid where multiplication is covariant, if one element has a preorder relation greater than or equal to one, then every power of that element is also greater than or equal to one.
|
pow_right_strictMono'
theorem pow_right_strictMono' :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : M},
1 < a → StrictMono fun x => a ^ x
The theorem `pow_right_strictMono'` asserts that for any type `M` which is a monoid and a preorder, and where the multiplication operation is covariant in both the less-than and less-than-or-equal-to relation, if `a` is an element of `M` such that `1 < a`, then the function that maps `x` to `a ^ x` is strictly monotone. In other words, if we have a monoid `M` that is also ordered and `a` is an element from `M` that is greater than 1, then for any two natural numbers `n` and `m`, if `n < m`, it implies that `a^n < a^m`.
More concisely: For any monoid `M` with a covariant multiplication operation in a preorder, if `1 < a` in `M`, then the function `x => a ^ x` is strictly increasing.
|
StrictMono.nsmul_left
theorem StrictMono.nsmul_left :
∀ {β : Type u_1} {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [inst_2 : Preorder β]
[inst_3 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_4 : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {f : β → M},
StrictMono f → ∀ {n : ℕ}, n ≠ 0 → StrictMono fun x => n • f x
The theorem `StrictMono.nsmul_left` asserts that for any strictly monotone function `f` from a preordered type `β` to an additive monoid `M` (which is also preordered), where `M` satisfies certain covariance properties, if we scale `f` by a non-zero natural number `n`, the resulting function remains strictly monotone. In other words, given a strictly monotone function, multiplying the output of the function by a non-zero natural number preserves its strict monotonicity.
More concisely: If `f` is a strictly monotone function from a preordered type `β` to an additive monoid `M` with covariance properties, then the scaled function `x mapsto n * f(x)` is also strictly monotone for any non-zero natural number `n`.
|
nsmul_nonneg
theorem nsmul_nonneg :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : M}, 0 ≤ a → ∀ (n : ℕ), 0 ≤ n • a
This theorem states that for any type `M` that is an ordered additive monoid (i.e., a structure with an addition operation and an order relation that respects this addition), if an element `a` of `M` is nonnegative (i.e., greater than or equal to zero), then the `n`-fold sum of `a` (denoted `n • a`), for any natural number `n`, is also nonnegative. In other words, repeatedly adding a nonnegative element to itself any number of times keeps the result nonnegative.
More concisely: For any ordered additive monoid `M` and non-negative element `a` in `M`, the `n`-fold sum `n • a` is non-negative for all natural numbers `n`.
|
nsmul_le_nsmul_left
theorem nsmul_le_nsmul_left :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : M} {n m : ℕ},
0 ≤ a → n ≤ m → n • a ≤ m • a
This theorem, `nsmul_le_nsmul_left`, states that for any type `M` that is an additive monoid and has an order (`Preorder`) and covariance property, given any element `a` of `M` and two natural numbers `n` and `m`, if `a` is nonnegative (`0 ≤ a`) and `n` is less than or equal to `m` (`n ≤ m`), then multiplying `a` by `n` (denoted as `n • a`) is less than or equal to multiplying `a` by `m` (denoted as `m • a`). This is essentially a generalized version of the property that in any ordered monoid, multiplication respects the order of its operands.
More concisely: For any additive monoid M with order and covariance property, if 0 ≤ a and n ≤ m in N, then n • a ≤ m • a.
|
pow_strictMono_left
theorem pow_strictMono_left :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : M},
1 < a → StrictMono fun x => a ^ x
The theorem `pow_strictMono_left` states that for any type `M` which has a monoid structure and a preorder structure, and is also covariant in multiplication, if an element `a` of this type satisfies `1 < a`, then the function `x ↦ a ^ x` is strictly monotone. In other words, if we have an element `a` in a monoid `M` which is greater than `1`, then raising `a` to higher powers gives larger results; if `x < y`, then `a ^ x < a ^ y`.
More concisely: For any monoid `M` with a preorder and covariance in multiplication, if `1 < a` in `M`, then the function `x ↦ a ^ x` is strictly increasing.
|
pow_le_pow_of_le_left'
theorem pow_le_pow_of_le_left' :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : M},
a ≤ b → ∀ (i : ℕ), a ^ i ≤ b ^ i
This theorem, labelled as an "Alias of `pow_le_pow_left'`", asserts a result about the powers of elements in a certain type of mathematical structure. Specifically, it states that for any type 'M', under the conditions that 'M' is a monoid, a preorder, and satisfies two additional covariant classes (related to the structure's multiplication and less than or equal relation), if 'a' and 'b' are elements of 'M' and 'a' is less than or equal to 'b', then for any natural number 'i', 'a' to the power of 'i' is less than or equal to 'b' to the power of 'i'.
More concisely: For any monoid M with a preorder and the given covariant properties, if a ≤ b in M, then a^i ≤ b^i for all natural numbers i.
|
pow_strictMono_right'
theorem pow_strictMono_right' :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
[inst_3 : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {n : ℕ},
n ≠ 0 → StrictMono fun x => x ^ n
The theorem `pow_strictMono_right'` states that for any type `M` that has a monoid structure and a preorder relation, and is covariant under multiplication (both from left and right), the function that raises `x` to a non-zero natural number exponent `n` is strictly increasing. That is, if `a` and `b` are elements of `M` with `a < b`, then `a^n < b^n`. The condition `n ≠ 0` rules out the zero exponent case where `a^0 = b^0 = 1` for all `a` and `b` in `M`. This theorem is an alias of the `pow_left_strictMono` theorem.
More concisely: For any covariant monoid `M` with a preorder relation, the function `x => x ^ n` is strictly increasing on `M` for `n ≠ 0`.
|
pow_mono_right
theorem pow_mono_right :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (n : ℕ),
Monotone fun a => a ^ n
The theorem `pow_mono_right` states that for any type `M` that is a monoid and a preorder, and in which multiplication preserves the order relation from both sides (i.e., if `x ≤ y` then `x * z ≤ y * z` and `z * x ≤ z * y` for all `x, y, z` in `M`), exponentiation with a fixed natural number exponent `n` is a monotone function. The latter means that if `a ≤ b` then `a^n ≤ b^n` for all `a, b` in `M`. This theorem is an alias of the `pow_left_mono` theorem.
More concisely: If `M` is a monoid and a preorder where multiplication preserves the order relation from both sides, then exponentiation with a fixed natural number exponent is a monotone function, i.e., for all `a, b` in `M` with `a ≤ b`, it holds that `a^n ≤ b^n` for some `n` in `ℕ`.
|
nsmul_le_nsmul_right
theorem nsmul_le_nsmul_right :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : M},
a ≤ b → ∀ (i : ℕ), i • a ≤ i • b
The theorem `nsmul_le_nsmul_right` states that for any type `M` which is an additive monoid and a preorder, and if it satisfies the covariant properties for addition and ordering, then for any two elements `a` and `b` of `M` such that `a` is less than or equal to `b`, the scalar multiplication of `a` by any natural number `i` is also less than or equal to the scalar multiplication of `b` by the same natural number `i`. More intuitively, this means that if an element `a` is less than or equal to an element `b` in this type `M`, then any 'multiple' of `a` is also less than or equal to the corresponding 'multiple' of `b`.
More concisely: For any additive monoid and preorder type `M` with covariant properties for addition and ordering, if `a ≤ b` in `M`, then for all natural numbers `i`, `i*a ≤ i*b`.
|
le_of_pow_le_pow'
theorem le_of_pow_le_pow' :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M]
[inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
[inst_3 : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b : M} {n : ℕ},
n ≠ 0 → a ^ n ≤ b ^ n → a ≤ b
This theorem states that in a monoid `M` that is also a linear order, if the multiplication operation is covariant (i.e., `x * y < x' * y'` whenever `x < x'` and `y < y'`, and this holds true even when the order of multiplication is swapped), then for any two elements `a` and `b` of `M` and a non-zero natural number `n`, if `a` raised to the power of `n` is less than or equal to `b` raised to the power of `n`, then `a` is less than or equal to `b`. The theorem applies to structures that combine aspects of algebra (the monoid structure) and order theory (the linear order structure), and is essentially a generalization of a property of real numbers.
More concisely: In a monoid with a covariant multiplication operation that is also a linear order, if `a^n <= b^n` for some natural number `n` and elements `a` and `b`, then `a <= b`.
|
pow_lt_pow_iff'
theorem pow_lt_pow_iff' :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M]
[inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : M} {m n : ℕ},
1 < a → (a ^ m < a ^ n ↔ m < n)
This theorem, `pow_lt_pow_iff'`, is an alias for `pow_lt_pow_iff_right'`. It states that, for any type `M` that is a monoid and a linear order, with two specific covariance conditions, and any element `a` of `M` and natural numbers `m` and `n`, if `a` is greater than 1, then `a` raised to the power `m` is less than `a` raised to the power `n` if and only if `m` is less than `n`.
More concisely: For any monoid and linear order type `M` satisfying specific covariance conditions and any `a : M` with `a > 1`, `a^m < a^n` if and only if `m < n`.
|
pow_le_pow'
theorem pow_le_pow' :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : M} {n m : ℕ},
1 ≤ a → n ≤ m → a ^ n ≤ a ^ m
This theorem, `pow_le_pow'`, states that for any type `M` that is a monoid and has a preorder relation, and satisfies the 'covariant' condition (that multiplying elements does not reverse the order), if `a` is an element of `M` and `n` and `m` are natural numbers such that `a` is greater than or equal to 1 and `n` is less than or equal to `m`, then `a` to the power of `n` is less than or equal to `a` to the power of `m`. In other words, raising a non-negative element to a higher power results in a greater or equal value in this ordered monoid context.
More concisely: For all monoids M with a preorder relation and the covariant condition, if 0 < a in M and n <= m are natural numbers, then a^n <= a^m.
|
nsmul_le_nsmul_iff
theorem nsmul_le_nsmul_iff :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : M} {m n : ℕ},
0 < a → (m • a ≤ n • a ↔ m ≤ n)
The theorem `nsmul_le_nsmul_iff` is an alias of `nsmul_le_nsmul_iff_left`. It states that for any type `M` that is an additive monoid and has a linear order, and for any instances where addition (`x + x_1`) is covariant in both the non-strict (`x ≤ x_1`) and strict (`x < x_1`) orders, then for any element `a` of `M` and natural numbers `m` and `n`, if `a` is positive (`0 < a`), then `m` times `a` is less than or equal to `n` times `a` if and only if `m` is less than or equal to `n`. This implies that multiplication by a positive element preserves the order of natural numbers.
More concisely: For any additive monoid with a linear order where addition is covariant in the order, if `0 < a` in the monoid and `m ≤ n` are natural numbers, then `m * a ≤ n * a`.
|
pow_left_strictMono
theorem pow_left_strictMono :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
[inst_3 : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {n : ℕ},
n ≠ 0 → StrictMono fun x => x ^ n
The theorem `pow_left_strictMono` states that for any type `M` that forms a monoid and has a preorder structure, if the operations of multiplication and comparison are covariant, then for any non-zero natural number `n`, the function that takes `x` to the `n`th power of `x` is strictly monotone. In other words, if `a` and `b` are elements of `M` such that `a < b`, then `a^n < b^n`.
More concisely: For any monoid `M` with covariant multiplication and preorder structure, the function from `M` to itself that maps each element to its `n`th power is strictly monotone on the positive elements.
|
StrictMono.pow_right'
theorem StrictMono.pow_right' :
∀ {β : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [inst_2 : Preorder β]
[inst_3 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
[inst_4 : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {f : β → M},
StrictMono f → ∀ {n : ℕ}, n ≠ 0 → StrictMono fun x => f x ^ n
This theorem, `StrictMono.pow_right'`, states that for any types `β` and `M`, where `M` is a monoid and `β` is preordered, and given a function `f` from `β` to `M`, if the function is strictly monotone, then the function `f` raised to a non-zero natural number `n` (represented as `f x ^ n`) will also be strictly monotone. In other words, if `f` is strictly increasing, then so is `f` to the power `n`, provided `n` is not zero. We also require two covariance conditions for multiplication on `M` to ensure the order-preserving properties we need.
More concisely: If `f : β -> M` is a strictly monotone function between a preordered type `β` and a monoid `M` with covariant multiplication, then `f ^ n : β -> M` is also strictly monotone for any non-zero natural number `n`.
|
pow_le_pow_of_le_one'
theorem pow_le_pow_of_le_one' :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : M} {n m : ℕ},
a ≤ 1 → n ≤ m → a ^ m ≤ a ^ n
This theorem states that for any type `M` which has a monoid structure and a preorder relation, and also satisfies the covariant class condition, given an element `a` of type `M` and two natural numbers `n` and `m`, if `a` is less than or equal to 1 and `n` is less than or equal to `m`, then `a` raised to the power `m` is less than or equal to `a` raised to the power `n`. In short, for a monoid under certain conditions, if `a ≤ 1` and `n ≤ m`, then `a^m ≤ a^n`.
More concisely: For any monoid endowed with a preorder relation and satisfying the covariant class condition, if 1 exceeds an element `a` and natural number `n` is less than or equal to `m`, then `a^m` is less than or equal to `a^n`.
|
nsmul_le_nsmul_of_nonpos
theorem nsmul_le_nsmul_of_nonpos :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : M} {n m : ℕ},
a ≤ 0 → n ≤ m → m • a ≤ n • a
This theorem, `nsmul_le_nsmul_of_nonpos`, is essentially an alias of `nsmul_le_nsmul_left_of_nonpos`. It states that for any type `M` that is an add monoid and has a preorder, and is covariant in two operations (addition and less than or equal to), given two natural numbers `n` and `m`, and an element `a` of `M` such that `a` is less than or equal to zero, if `n` is less than or equal to `m`, then `m` times `a` is less than or equal to `n` times `a`. Here, the "times" operation refers to the n-times repeated addition (also known as scalar multiplication) from the add monoid structure.
More concisely: For any add monoid M with a preorder covariant in two operations, and any natural numbers n, m, and element a of M with a <= 0, if n <= m then n*a <= m*a.
|
nsmul_le_nsmul
theorem nsmul_le_nsmul :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : M} {n m : ℕ},
0 ≤ a → n ≤ m → n • a ≤ m • a
This theorem states that for any type `M` that is an additively monoidal and preordered, where the monoid operation and ordering are compatible (as specified by the `CovariantClass`), if `a` is a non-negative element of `M` and `n` is less than or equal to `m`, then the `n`-fold sum of `a` (denoted by `n • a`) is less than or equal to the `m`-fold sum of `a` (denoted by `m • a`). This is essentially a property of ordered monoidal structures.
More concisely: For any additively monoidal and preordered type `M` with CovariantClass, if `a` is a non-negative element and `n <= m`, then `n * a <= m * a`. Here, `*` denotes both the monoid operation and scalar multiplication in the context of an additively monoidal structure.
|
one_le_pow_iff
theorem one_le_pow_iff :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M]
[inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {x : M} {n : ℕ},
n ≠ 0 → (1 ≤ x ^ n ↔ 1 ≤ x)
This theorem states that for any type `M` with a monoid, linear order, and covariant class structure, and for any element `x` of type `M` and natural number `n`, given that `n` is not zero, `1` is less than or equal to `x` raised to the power of `n` if and only if `1` is less than or equal to `x`. In mathematical terms, for all $x$ in some ordered monoid $M$ and all $n$ in $\mathbb{N}$ with $n \neq 0$, $1 \leq x^n$ if and only if $1 \leq x$.
More concisely: For any ordered monoid $M$ and $x$ in $M$ with $n$ a non-zero natural number, $1 \leq x^n$ if and only if $1 \leq x$.
|
pow_le_pow_iff'
theorem pow_le_pow_iff' :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M]
[inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : M} {m n : ℕ},
1 < a → (a ^ m ≤ a ^ n ↔ m ≤ n)
The theorem `pow_le_pow_iff'` states that for a given type `M` that forms a monoid and a linear order, and satisfies two covariant classes (which essentially state that multiplication is compatible with the order `≤` and `<` respectively), if `a` is an element of `M` such that `1 < a` and `m` and `n` are natural numbers, then `a` raised to the power `m` is less than or equal to `a` raised to the power `n` if and only if `m` is less than or equal to `n`. This basically means that for such a specified `a`, the power function is an increasing function.
More concisely: For all types `M` that form a monoid and a linear order with covariant multiplication order properties, and for all `a` in `M` with `1 < a`, the inequality `a^m <= a^n` holds if and only if `m <= n`.
|
lt_of_nsmul_lt_nsmul_right
theorem lt_of_nsmul_lt_nsmul_right :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : M} (n : ℕ),
n • a < n • b → a < b
The theorem `lt_of_nsmul_lt_nsmul_right` states that for any type `M` that is an additive monoid and a linearly ordered set, where both the normal addition operation and its swapped version are covariant i.e., if `x ≤ y` then `x + z ≤ y + z` and `z + x ≤ z + y` for all `x, y, z` in `M`, then whenever the `n`-fold sum of `a` (denoted `n • a`) is less than the `n`-fold sum of `b` (denoted `n • b`), it follows that `a` is less than `b`. This is for any natural number `n` and any `a, b` in `M`. In other words, if the repeated sum of `a` is less than the repeated sum of `b`, then `a` itself must be less than `b`.
More concisely: If `M` is an additive monoid and a linearly ordered set where the normal and swapped addition operations are covariant, then for all natural numbers `n` and elements `a, b` in `M`, if `n • a` is strictly less than `n • b`, then `a` is strictly less than `b`.
|
nsmul_left_strictMono
theorem nsmul_left_strictMono :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : M},
0 < a → StrictMono fun x => x • a
The theorem `nsmul_left_strictMono` states that for any type `M` that is an additive monoid and a preorder, and where addition (`x + x_1`) is covariant in both the `≤` and `<` preorders, if `a` is an element of `M` such that `0 < a`, then the function `fun x => x • a` (which represents scalar multiplication of `a` by `x`) is strictly monotonic. In other words, for any two elements `x` and `y` in `M`, if `x < y`, then `x • a < y • a`.
More concisely: For any additive monoid and preorder type `M` where addition is covariant in the preorders `≤` and `<`, and for any `0 < a` in `M`, the function `x => x • a` is strictly monotonic: if `x < y` in `M`, then `x • a < y • a`.
|
lt_of_pow_lt_pow_left'
theorem lt_of_pow_lt_pow_left' :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M]
[inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : M} (n : ℕ),
a ^ n < b ^ n → a < b
The theorem `lt_of_pow_lt_pow_left'` asserts that for any types `M` that forms a monoid and has a linear order, with two additional properties expressed by the `CovariantClass` conditions. The properties describe the relationship between multiplication and the order relation in `M`. Given any two elements `a` and `b` of `M` and a natural number `n`, if `a` raised to the power `n` is less than `b` raised to the power `n`, then `a` is less than `b`. In other words, this theorem captures the fact that the power function preserves the order relation in a monoid that also has a linear order and satisfies the specified covariance conditions.
More concisely: For any monoid `M` with a linear order and satisfying the given covariance conditions, if `a^n < b^n` for some natural number `n`, then `a < b`.
|
nsmul_strictMono_left
theorem nsmul_strictMono_left :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_3 : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {n : ℕ},
n ≠ 0 → StrictMono fun x => n • x
The theorem `nsmul_strictMono_left` states that for any type `M` which is an `AddMonoid` and a `Preorder`, and for which addition is covariant in both arguments (meaning, roughly, that increasing the arguments increases the result), if `n` is a natural number different from zero, then the function which maps `x` to `n` times `x` (denoted as `n • x`) is strictly monotone. In other words, if `a` and `b` are elements of `M` such that `a < b`, then `n • a < n • b`. This is essentially a generalization of the fact that multiplication by a positive number preserves the order of elements in the ordered semigroup of non-negative real numbers.
More concisely: For any AddMonoid and Preorder type M with covariant addition, the function n • x (n times x) is strictly monotone on M, i.e., if a < b in M, then n • a < n • b.
|
nsmul_nonneg_iff
theorem nsmul_nonneg_iff :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {x : M} {n : ℕ},
n ≠ 0 → (0 ≤ n • x ↔ 0 ≤ x)
This theorem states that for any type `M` which is an additive monoid and has a linear order, and for any variable `x` of type `M` and natural number `n`, if `n` is not zero, then `n` times `x` is nonnegative if and only if `x` is nonnegative. This essentially means that the non-negativity of a scalar multiple in a linearly ordered monoid is equivalent to the non-negativity of the original element, provided the scalar itself is non-zero.
More concisely: For any additive monoid M with a linear order, and for all x in M and natural number n, the product x * n is non-negative if and only if x is non-negative.
|
nsmul_pos
theorem nsmul_pos :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : M},
0 < a → ∀ {k : ℕ}, k ≠ 0 → 0 < k • a
The theorem `nsmul_pos` states that for all instances of an additive monoid `M` that also have a pre-order relation and a covariant class, if a non-zero element `a` of `M` is greater than zero, then for any non-zero natural number `k`, the n-times sum (or n-smultiplication) of `a` (denoted as `k • a`) is also greater than zero. This means that repeated addition of a positive value in this structure will always yield a result that's still positive, as long as the number of repetitions is non-zero.
More concisely: For any additive monoid with a pre-order relation and a covariant class, if 0 < a in M and n is a non-zero natural number, then n • a > 0.
|
nsmul_right_strictMono
theorem nsmul_right_strictMono :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_3 : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {n : ℕ},
n ≠ 0 → StrictMono fun x => n • x
The theorem `nsmul_right_strictMono` states that, for any type `M` which is an ordered additive monoid, and for any natural number `n` that is not zero, the function that maps `x` to `n` multiplied by `x` (denoted as `n • x`) is strictly monotone. In other words, if `a` and `b` are elements of `M` and `a < b`, then `n • a < n • b`. This implies that multiplying by a non-zero natural number preserves the order in an ordered additive monoid.
More concisely: For any ordered additive monoid type `M` and non-zero natural number `n`, the function `n • x` mapping `x` to `n` times `x` is a strict order preserving function on `M`.
|
lt_of_nsmul_lt_nsmul
theorem lt_of_nsmul_lt_nsmul :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : M} (n : ℕ),
n • a < n • b → a < b
This theorem, `lt_of_nsmul_lt_nsmul`, states that for any type `M`, with an additive monoid structure and a linear order, and for any two elements `a` and `b` of `M`, if the `n`-fold sum of `a` (denoted as `n • a`) is strictly less than the `n`-fold sum of `b` (`n • b`), then `a` is strictly less than `b`. The theorem assumes that the order is compatible with the monoid operation, in both the direct and swapped arguments sense. This is known as the covariant property.
More concisely: If for all natural numbers `n`, `n • a` is strictly less than `n • b` in a types `M` with an additive monoid structure and a linear order compatible with monoid multiplication, then `a` is strictly less than `b`.
|
nsmul_strictMono_right
theorem nsmul_strictMono_right :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : M},
0 < a → StrictMono fun x => x • a
The theorem `nsmul_strictMono_right` states that for any type `M` that has an addition operation forming a monoid, a preorder, and satisfies both the covariant class conditions for addition wrt. the `≤` and `<` relations, if `a` is an element of `M` such that `0 < a`, then the function that maps each element `x` to `x • a` (i.e., `a` added to itself `x` times) is strictly monotonic. In other words, if `x < y`, then `x • a < y • a`.
More concisely: For any monoid `M` with a preorder `≤` and covariant class conditions for addition, if `0 < a` in `M`, then the function `x mapsto x * a` is strictly increasing with respect to `≤`.
|
Monotone.nsmul_left
theorem Monotone.nsmul_left :
∀ {β : Type u_1} {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [inst_2 : Preorder β]
[inst_3 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {f : β → M},
Monotone f → ∀ (n : ℕ), Monotone fun a => n • f a
The theorem `Monotone.nsmul_left` states that for any type `β` and a type `M` which is an additive monoid and a preorder, where this monoid is both left and right covariant under the operation of addition, if `f` is a monotone function from `β` to `M`, then for any natural number `n`, the function that maps each element `a` in `β` to `n` times `f(a)` is also monotone. This essentially implies that monotonicity is preserved under scalar multiplication in this context.
More concisely: If `f` is a monotone function from a preorder `β` to an additive monoid `M` with covariant addition, then the function multiplying each element by a constant `n` and applying `f` is also monotone.
|
nsmul_lt_nsmul_iff
theorem nsmul_lt_nsmul_iff :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : M} {m n : ℕ},
0 < a → (m • a < n • a ↔ m < n)
The theorem `nsmul_lt_nsmul_iff` states that for any type `M` that is an additive monoid and a linear order, and it is covariant in both 'less than or equal to' (`≤`) and 'less than' (`<`) relation, given any positive element `a` of type `M` and any two natural numbers `m` and `n`, it holds that `m` times `a` is less than `n` times `a` if and only if `m` is less than `n`. Here, `m • a` and `n • a` represent the operation of adding `a` to itself `m` and `n` times respectively, also known as scalar multiplication in the context of monoids.
More concisely: For any additive monoid and linear order M with covariant less-than relations, and positive element a, m < n if and only if m • a < n • a, where m and n are natural numbers and • denotes scalar multiplication.
|
pow_lt_pow'
theorem pow_lt_pow' :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : M} {n m : ℕ},
1 < a → n < m → a ^ n < a ^ m
This theorem, `pow_lt_pow'`, states that for any type `M` that forms a monoid and two order relationships (one for `≤` and one for `<`) that are covariant with respect to multiplication, given two natural numbers `n` and `m` and an element `a` of `M` such that `1 < a` and `n < m`, the inequality `a^n < a^m` holds. Essentially, for a monoid element `a` that is greater than one and two natural numbers `n` and `m` where `n` is less than `m`, the power of `a` to `n` is less than the power of `a` to `m`.
More concisely: For any monoid `M` with covariant order relations `≤` and `<`, and `a` in `M` with `1 < a` and `n < m`, we have `a^n < a^m`.
|
le_of_nsmul_le_nsmul
theorem le_of_nsmul_le_nsmul :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_3 : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : M} {n : ℕ},
n ≠ 0 → n • a ≤ n • b → a ≤ b
The theorem `le_of_nsmul_le_nsmul` states that for any type `M` that is an additively structured monoid and a linearly ordered set, and for which the addition operation (`x + x_1`) is covariant (preserves the order), both in the direct and swapped arguments order, if you have elements `a` and `b` of type `M` and a natural number `n` which is not zero, then if `n` times `a` is less than or equal to `n` times `b`, it must be the case that `a` is less than or equal to `b`. In other words, this theorem states that if the n-fold addition (multiplication) of `a` is less than or equal to the n-fold addition of `b` for non-zero `n`, then `a` is less than or equal to `b`.
More concisely: For any additively structured monoid and linearly ordered set M with covariant addition, if n times a ≤ n times b for a, b ∈ M and non-zero natural number n, then a ≤ b.
|
pow_eq_one_iff
theorem pow_eq_one_iff :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M]
[inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {x : M} {n : ℕ},
n ≠ 0 → (x ^ n = 1 ↔ x = 1)
This theorem states that for any type `M` with the structures of a monoid and a linear order, and the covariant class property (indicating that multiplication is monotonically increasing), for any element `x` of `M` and any natural number `n` not equal to zero, the statement "`x` to the power of `n` equals 1" is logically equivalent to "`x` equals 1". In other words, in such a structure, the only way for a non-zero power of `x` to equal 1 is if `x` itself is 1.
More concisely: For any monoid with a covariant linear order structure where multiplication is monotonic, the power `x^n` equals 1 if and only if `x` equals 1.
|
nsmul_mono_left
theorem nsmul_mono_left :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (n : ℕ),
Monotone fun a => n • a
The theorem `nsmul_mono_left` states that for any natural number `n` and any type `M` that is an ordered additive monoid (meaning it has a binary operation of addition and an order relation that are compatible), the function that scales an element of `M` by `n` (denoted `n • a` for `a` in `M`) is a monotone function. In other words, if `a` and `b` are elements of `M` such that `a ≤ b`, then `n • a ≤ n • b`. This is a property that is especially important in the study of ordered algebraic structures.
More concisely: For any natural number `n` and any ordered additive monoid `M`, the scaling function `n •` is a monotone function on `M`.
|
nsmul_lt_nsmul_left
theorem nsmul_lt_nsmul_left :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : M} {n m : ℕ},
0 < a → n < m → n • a < m • a
The theorem `nsmul_lt_nsmul_left` states that for any type `M` that is an ordered additive monoid (it satisfies properties of an additive monoid and a preorder), if `a` is a positive element of `M` and `n` and `m` are natural numbers such that `n` is less than `m`, then the n-times repeated addition of `a` (denoted `n • a`) is less than the m-times repeated addition of `a` (denoted `m • a`).
More concisely: For any ordered additive monoid M, positive element a, and natural numbers n < m, n • a < m • a.
|
nsmul_lt_nsmul
theorem nsmul_lt_nsmul :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : M} {n m : ℕ},
0 < a → n < m → n • a < m • a
This theorem, which is an alias of `nsmul_lt_nsmul_left`, states that for any type `M` that is an additive monoid and a preorder, and also satisfies certain covariance properties, given any element `a` of type `M` and natural numbers `n` and `m`, if `a` is greater than `0` and `n` is less than `m`, then the `n`-fold sum of `a` is less than the `m`-fold sum of `a`. Essentially, it says that for positive elements of a certain type, scaling by a larger natural number results in a larger value.
More concisely: For any additive monoid and preorder type `M` satisfying certain covariance properties, if `0 < a : M` and `n < m : ℕ`, then `n * a < m * a`.
|
nsmul_le_nsmul_of_le_right
theorem nsmul_le_nsmul_of_le_right :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : M},
a ≤ b → ∀ (i : ℕ), i • a ≤ i • b
In natural language, the Lean theorem `nsmul_le_nsmul_of_le_right` can be described as follows:
For any type `M` that is an additive monoid and a preorder where addition is covariant in both arguments, if `a` and `b` are elements of `M` such that `a` is less than or equal to `b`, then for any natural number `i`, `i` times `a` is less than or equal to `i` times `b`. In other words, if `a` is less than or equal to `b`, then scaling `a` by a natural number does not make it greater than the corresponding scaling of `b`.
More concisely: For all additive monoids with covariant addition `M`, `i` in $\mathbb{N}$, and `a`, `b` in `M` with `a ≤ b`, we have `i * a ≤ i * b`.
|
pow_le_pow_left'
theorem pow_le_pow_left' :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : M},
a ≤ b → ∀ (i : ℕ), a ^ i ≤ b ^ i
This theorem, `pow_le_pow_left'`, states that for any type `M` equipped with a monoid structure, a preorder, and two covariant classes defined over the multiplication operation and a less-than-or-equal-to relation, if `a` and `b` are two elements of `M` such that `a` is less than or equal to `b`, then for any natural number `i`, `a` to the power of `i` is less than or equal to `b` to the power of `i`. In mathematical terms, this can be written as: for all `a, b ∈ M` and `i ∈ ℕ` such that `a ≤ b`, `a^i ≤ b^i`.
More concisely: For all types `M` with a monoid structure, preorder, and covariant multiplication and order classes, if `a ≤ b` in `M` then `a^n ≤ b^n` for all natural numbers `n`.
|
nsmul_right_mono
theorem nsmul_right_mono :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M]
[inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (n : ℕ),
Monotone fun a => n • a
The theorem `nsmul_right_mono` states that for any natural number `n` and any type `M` that is an additive monoid and a preorder, and for which addition is monotone increasing both on the left and on the right (i.e., satisfies the conditions of both `CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1` and `CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1`), the function that multiplies an element of `M` by `n` (denoted `n • a`) is also monotone increasing. In other words, if `a ≤ b` then `n • a ≤ n • b`, where `n • a` denotes the n-fold addition of `a` to itself.
More concisely: For any additive monoid M with monotone increasing addition on both sides and natural number n, the function n • (.) from M to M, defined as repeated addition (n-fold), is monotone increasing.
|