pos_and_pos_or_neg_and_neg_of_mul_pos
theorem pos_and_pos_or_neg_and_neg_of_mul_pos :
∀ {α : Type u_1} {a b : α} [inst : MulZeroClass α] [inst_1 : LinearOrder α] [inst_2 : PosMulMono α]
[inst_3 : MulPosMono α], 0 < a * b → 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
The theorem `pos_and_pos_or_neg_and_neg_of_mul_pos` asserts that for any type `α` with multiplication and zero, along with a linear order, and where multiplication is monotonic with respect to nonnegative elements both on the left and right, if the product of two elements `a` and `b` is positive, then either both `a` and `b` are positive, or both `a` and `b` are negative. This is a formalization of the elementary property of real numbers that the product of two numbers is positive if and only if the two numbers have the same sign.
More concisely: If `α` is a type with multiplication, zero, and a linear order such that multiplication is monotonic with respect to nonnegative elements on both sides, then `a * b` is positive if and only if either `a` or `b` is positive.
|
Right.one_lt_mul_of_lt_of_lt
theorem Right.one_lt_mul_of_lt_of_lt :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α]
[inst_3 : MulPosStrictMono α], 1 < a → 1 < b → 0 < b → 1 < a * b
The theorem `Right.one_lt_mul_of_lt_of_lt` represents a mathematical statement about ordered multiplication structures. It states that for any type `α` that has multiplication, one, zero, and a preorder, and for which multiplication by a positive number is strictly increasing, if `a` and `b` are elements of `α`, such that both `a` and `b` are greater than one and `b` is positive, then the product `a * b` is also greater than one. This essentially captures a property of positive multiplication in such ordered structures.
More concisely: If `α` is a type with multiplication, one, zero, preorder, and strictly increasing multiplication by positive numbers, then for all `a, b ∈ α` such that `a, b > 1` and `b > 0`, it holds that `a * b > 1`.
|
lt_of_mul_lt_mul_of_nonneg_left
theorem lt_of_mul_lt_mul_of_nonneg_left :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : PosMulReflectLT α],
a * b < a * c → 0 ≤ a → b < c
The theorem `lt_of_mul_lt_mul_of_nonneg_left` states that for any type `α` that supports multiplication, has a zero element, and is preordered, and additionally exhibits strict reverse monotonicity of multiplication by nonnegative elements on the left (as defined by the `PosMulReflectLT` typeclass), if the product of `a` and `b` is less than the product of `a` and `c`, and `a` is nonnegative, then `b` is less than `c`. In simpler terms, in a structure with these properties, if scaling `b` by `a` gives a smaller result than scaling `c` by the same nonnegative `a`, then `b` must be smaller than `c`.
More concisely: If `α` is a preordered type with zero, supports multiplication, and satisfies strict reverse monotonicity of multiplication by nonnegative elements on the left, then for all nonnegative `a` and `b`, `c` in `α` such that `a * b` is less than `a * c`, it follows that `b` is less than `c`.
|
Left.lt_mul_of_lt_of_one_le_of_nonneg
theorem Left.lt_mul_of_lt_of_one_le_of_nonneg :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : PosMulMono α],
1 < a → 1 ≤ b → 0 ≤ a → 1 < a * b
The theorem `Left.lt_mul_of_lt_of_one_le_of_nonneg` asserts that, for any type `α` with properties of multiplication, unity, zero, and a preorder, and additionally satisfying the property of positive multiplication monotonicity (`PosMulMono α`), if `a` and `b` are elements of `α` such that `1 < a`, `1 ≤ b`, and `0 ≤ a`, then it must be that `1 < a * b`. In other words, under certain conditions on `a` and `b`, multiplying `a` and `b` results in an element strictly greater than 1.
More concisely: If `α` is a type with multiplication, unity, zero, preorder, and positive multiplication monotonicity, and `1 < a` and `1 <= b` with `0 <= a`, then `1 < a * b`.
|
mul_lt_mul_left
theorem mul_lt_mul_left :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : PosMulStrictMono α]
[inst_4 : PosMulReflectLT α], 0 < a → (a * b < a * c ↔ b < c)
This theorem, `mul_lt_mul_left`, states that for any type `α` equipped with multiplication, a zero element, and a preorder relation, and satisfying the properties of strict monotonicity of multiplication by positive elements on the left (`PosMulStrictMono α`) and strict reverse monotonicity of multiplication by nonnegative elements on the left (`PosMulReflectLT α`), if `0 < a`, then the product of `a` and `b` is less than the product of `a` and `c` if, and only if, `b` is less than `c`. This embeds the property of 'cancellation' in these algebraic structures, stating that multiplying a smaller number by a positive number yields a smaller product.
More concisely: If `α` is a type with multiplication, a zero element, and preorder relation such that multiplication by positive elements is strictly monotonic on the left and multiplication by nonnegative elements is strictly reverse monotonic on the left, then `a > 0` implies `a * b < a * c` if and only if `b < c`.
|
le_of_mul_le_mul_left
theorem le_of_mul_le_mul_left :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : PosMulReflectLE α],
a * b ≤ a * c → 0 < a → b ≤ c
The theorem `le_of_mul_le_mul_left` is a statement about the behavior of multiplication in relation to order in certain mathematical structures. Specifically, it applies to any type `α` that has a multiplication operation (`Mul α`), a zero element (`Zero α`), and an order relation that is a preorder (`Preorder α`). Furthermore, this order relation must satisfy the property of reverse monotonicity of multiplication by positive elements on the left (`PosMulReflectLE α`), which basically means that if you multiply a smaller number by a positive number, the result is also smaller. The theorem itself states that for any elements `a`, `b`, and `c` of type `α`, if `a * b` is less than or equal to `a * c` and `a` is positive, then `b` must be less than or equal to `c`. In other words, if multiplying by `a` doesn't change the order of `b` and `c`, then `b` and `c` must have already been in that order.
More concisely: If `α` is a preordered type with a positive multiplication operation such that `a * b ≤ a * c` implies `b ≤ c`, then `a > 0` implies `b ≤ c`.
|
mul_lt_of_lt_one_right
theorem mul_lt_of_lt_one_right :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α]
[inst_3 : PosMulStrictMono α], 0 < a → b < 1 → a * b < a
This theorem states that for any given type `α` which has multiplication, an identity element for multiplication, zero, and a preorder (a reflexive and transitive relation), and satisfies the property of strict monotonicity of multiplication by positive elements (defined by `PosMulStrictMono α`), if `a` is a positive element and `b` is less than one, then the product of `a` and `b` is less than `a`. In mathematical terms, this can be stated as: if 0 < a and b < 1, then a * b < a.
More concisely: For any type `α` with multiplication, an identity element, zero, a preorder, and strict monotonicity of multiplication by positive elements, if `a` is positive and `b` is less than one, then `a * b` is less than `a`.
|
Right.mul_lt_one_of_le_of_lt_of_nonneg
theorem Right.mul_lt_one_of_le_of_lt_of_nonneg :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : MulPosMono α],
a ≤ 1 → b < 1 → 0 ≤ b → a * b < 1
The theorem `Right.mul_lt_one_of_le_of_lt_of_nonneg` states that given a type `α` that has multiplication and one, is ordered, and supports the notion of nonnegative multiplication, for any two elements `a` and `b` of `α`, if `a` is less than or equal to 1, `b` is less than 1, and `b` is nonnegative, then the product of `a` and `b` is less than 1. This is often used in the context of ordered ring structures where multiplication behaves in a certain way with respect to order and non-negativity.
More concisely: Given an ordered type `α` with multiplication and a non-negative element `b` less than 1, if `a` is also less than or equal to 1, then `a * b` is less than 1.
|
mul_le_of_le_one_right
theorem mul_le_of_le_one_right :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : PosMulMono α],
0 ≤ a → b ≤ 1 → a * b ≤ a
This theorem states that for a given type `α` that supports multiplication and has a special element called "one", has a zero element, and has a preorder relation (which gives us the concepts of "less than or equal to" and "greater than or equal to"), and is also a positive multiplicative monotonically ordered set (where multiplication by a nonnegative element does not change the order), if `a` is a nonnegative element of this type and `b` is an element of this type which is less than or equal to one, then the product `a * b` is less than or equal to `a`. This theorem is essentially stating that if you multiply a nonnegative number by a number that is less than or equal to one, the result will not exceed the original nonnegative number.
More concisely: For any non-negative element `a` and element `b` less than or equal to one in a type with multiplication, a preorder relation, and positive multiplicative monotonicity, `a * b` is less than or equal to `a`.
|
mul_le_mul
theorem mul_le_mul :
∀ {α : Type u_1} {a b c d : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulMono α]
[inst_3 : MulPosMono α], a ≤ b → c ≤ d → 0 ≤ c → 0 ≤ b → a * c ≤ b * d
The theorem `mul_le_mul` states that for any type `α` that has a multiplication operation, a zero element, and a preorder relation, and also satisfies the properties of monotonicity of multiplication by non-negative elements on both the left (PosMulMono) and the right (MulPosMono), if `a ≤ b` and `c ≤ d` are true and both `c` and `b` are non-negative (i.e., `0 ≤ c` and `0 ≤ b`), then `a * c ≤ b * d` is also true. This theorem therefore asserts the monotonicity of multiplication under certain conditions in the context of ordered algebraic structures.
More concisely: If `α` is an ordered algebraic structure with monotonic multiplication by non-negative elements (both left and right), then for all non-negative `a ≤ b` and `c ≤ d`, we have `a * c ≤ b * d`.
|
le_mul_of_one_le_left
theorem le_mul_of_one_le_left :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : MulPosMono α],
0 ≤ b → 1 ≤ a → b ≤ a * b
The theorem `le_mul_of_one_le_left` states that for any type `α` that has multiplication (`MulOneClass α`), zero (`Zero α`), and a preorder relation (`Preorder α`), and where multiplication is monotonically increasing when multiplying by nonnegative elements on the right (`MulPosMono α`), if `b` is nonnegative (`0 ≤ b`) and `a` is greater than or equal to one (`1 ≤ a`), then `b` is less than or equal to the product of `a` and `b` (`b ≤ a * b`). In simpler terms, in such a mathematical setting, multiplying any nonnegative number by a number that is at least one will result in a product that is greater than or equal to the original number.
More concisely: For any type `α` with `MulOneClass α`, `Zero α`, `Preorder α`, and `MulPosMono α`, if `0 ≤ b` and `1 ≤ a`, then `b ≤ a * b`.
|
mul_nonpos_of_nonpos_of_nonneg
theorem mul_nonpos_of_nonpos_of_nonneg :
∀ {α : Type u_1} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : MulPosMono α],
a ≤ 0 → 0 ≤ b → a * b ≤ 0
The theorem `mul_nonpos_of_nonpos_of_nonneg` states that for all types `α` with instances of `MulZeroClass`, `Preorder`, and `MulPosMono`, and for all elements `a` and `b` of type `α`, if `a` is less than or equal to 0 and `b` is greater than or equal to 0, then the product of `a` and `b` is less than or equal to 0. In simpler terms, in a context where multiplication and ordering behave as expected, if one factor is nonpositive and the other is nonnegative, their product will be nonpositive.
More concisely: If `a` is of type `α` with `MulZeroClass`, `Preorder`, and `MulPosMono instances`, and `a ≤ 0` and `b ≥ 0`, then `a * b ≤ 0`.
|
Left.mul_lt_of_lt_of_le_one_of_nonneg
theorem Left.mul_lt_of_lt_of_le_one_of_nonneg :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : PosMulMono α],
a < 1 → b ≤ 1 → 0 ≤ a → a * b < 1
This theorem, `Left.mul_lt_of_lt_of_le_one_of_nonneg`, asserts that for any type `α` equipped with a multiplication operation, a multiplicative identity (`1`), a zero, and a preorder relation (a reflexive and transitive binary relation), and assuming that multiplication by nonnegative elements on the left is monotonic, if `a` and `b` are elements of this type such that `a` is less than `1`, `b` is less than or equal to `1`, and `a` is nonnegative (greater than or equal to `0`), then the product `a * b` is less than `1`. Essentially, it guarantees that under these conditions, the product of `a` and `b` will be strictly less than the multiplicative identity, `1`.
More concisely: For any type equipped with a multiplication, identity, zero, preorder relation, and left-monotonicity of multiplication by nonnegative elements, if `a` is a nonnegative, less-than-one element, then `a * b` is less than 1 whenever `b` is less than or equal to 1.
|
mul_le_mul_of_nonneg_right
theorem mul_le_mul_of_nonneg_right :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : MulPosMono α],
b ≤ c → 0 ≤ a → b * a ≤ c * a
This is a theorem about the monotonicity of multiplication in an ordered semiring. It states that, given any type `α` that has a multiplication operation, zero, and is a preorder, and is also equipped with a property that multiplication by nonnegative elements (`a`) on the right is monotonic. If `b` is less than or equal to `c` and `a` is nonnegative (i.e., greater than or equal to zero), then `b` times `a` is less than or equal to `c` times `a`. In other words, if you multiply `b` and `c` (where `b ≤ c`) by the same nonnegative number `a`, the inequality relationship between `b` and `c` is preserved.
More concisely: If `α` is an ordered semiring with right multiplicatively monotonic nonnegative elements, then for all `a ≥ 0` and `b ≤ c` in `α`, we have `b * a ≤ c * a`.
|
mul_lt_mul_iff_of_pos_left
theorem mul_lt_mul_iff_of_pos_left :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : PosMulStrictMono α]
[inst_4 : PosMulReflectLT α], 0 < a → (a * b < a * c ↔ b < c)
The theorem `mul_lt_mul_iff_of_pos_left` states that for any type `α` with multiplication, a zero element, and a preorder relation, and where multiplication by positive elements on the left is strictly monotonic and strictly reverse monotonic for nonnegative elements, then for any elements `a`, `b`, and `c` of `α`, if `a` is positive, then `a * b` is less than `a * c` if and only if `b` is less than `c`. In mathematical terms, if `0 < a`, then `a * b < a * c` is equivalent to `b < c`.
More concisely: For all types `α` with multiplication, zero element, and preorder relation, if `0 < a` and multiplication by `a` is strictly monotonic and reverse monotonic on the left and nonnegative elements, then `a * b < a * c` if and only if `b < c`.
|
pos_of_mul_pos_left
theorem pos_of_mul_pos_left :
∀ {α : Type u_1} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : MulPosReflectLT α],
0 < a * b → 0 ≤ b → 0 < a
The theorem `pos_of_mul_pos_left` states that for any type `α` that has multiplication and zero, and is equipped with a preorder relation (`≤`) which reflects strict reverse monotonicity of multiplication by nonnegative elements on the right, if the product of two elements `a` and `b` in `α` is positive (i.e., `0 < a * b`), and `b` is nonnegative (i.e., `0 ≤ b`), then `a` must be positive (i.e., `0 < a`). In other words, if a non-negative number times another number gives a positive result, then the other number is positive. This is an important property related to the order of multiplication in ordered semirings.
More concisely: If `0 < a * b` and `0 <= b` in an ordered semiring, then `0 < a`.
|
le_of_mul_le_mul_right
theorem le_of_mul_le_mul_right :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : MulPosReflectLE α],
b * a ≤ c * a → 0 < a → b ≤ c
This theorem states that for any type `α` that is a preordered semiring (denoted by `Mul α`, `Zero α`, and `Preorder α`), and also satisfies the property of reverse monotonicity of multiplication by positive elements on the right (denoted by `MulPosReflectLE α`), if the product of `b` and `a` is less than or equal to the product of `c` and `a`, and `a` is positive (greater than zero), then `b` is less than or equal to `c`.
In other words, the theorem says that in such a structure, one can cancel a positive factor from both sides of an inequality. This is a form of the "cancellation law" for multiplication in ordered semirings.
More concisely: If `α` is a preordered semiring with reverse monotonicity of multiplication by positive elements and `a > 0`, then `b ≤ c` implies `a * b ≤ a * c`.
|
Right.one_lt_mul_of_lt_of_le_of_pos
theorem Right.one_lt_mul_of_lt_of_le_of_pos :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α]
[inst_3 : MulPosStrictMono α], 1 < a → 1 ≤ b → 0 < b → 1 < a * b
The theorem `Right.one_lt_mul_of_lt_of_le_of_pos` is about multiplication in a structure that has a multiplication operation, a multiplicative identity, a zero, and a preorder (a reflexive and transitive binary relation). Given a type `α` with these properties and the additional property of strict monotonicity of multiplication by positive elements on the right, the theorem states that for any two elements `a` and `b` of type `α`, if `a` is greater than the multiplicative identity, `b` is at least the multiplicative identity, and `b` is positive, then the product `a * b` is greater than the multiplicative identity. In mathematical terms, if 1 < a, 1 ≤ b, and 0 < b, then 1 < a * b.
More concisely: If $1 < a$ and $0 < b$ with $b$ being positive in a preordered monoid with strict right multiplicative identity, then $a \cdot b > 1$.
|
le_of_mul_le_mul_of_pos_left
theorem le_of_mul_le_mul_of_pos_left :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : PosMulReflectLE α],
a * b ≤ a * c → 0 < a → b ≤ c
The theorem `le_of_mul_le_mul_of_pos_left` states that for any type `α` equipped with multiplication, zero element, a preorder relation (such as less than or equal to), and exhibits positive reverse left monotonicity in multiplication, if `a * b` is less than or equal to `a * c` and `a` is greater than zero, then `b` is less than or equal to `c`. In other words, for positive `a`, if `a * b` is less than or equal to `a * c`, then `b` is less than or equal to `c`. This is a specific case of the principle that if you multiply two quantities and the result is smaller (or equal), then the factor you multiplied by must be smaller (or equal) if the multiplier is positive.
More concisely: For all types `α` with multiplication, zero element, and preorder `≤`, if `a ≥ 0`, `a * b ≤ a * c`, then `b ≤ c`.
|
Left.mul_lt_of_le_of_lt_one_of_pos
theorem Left.mul_lt_of_le_of_lt_one_of_pos :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α]
[inst_3 : PosMulStrictMono α], a ≤ 1 → b < 1 → 0 < a → a * b < 1
The theorem `Left.mul_lt_of_le_of_lt_one_of_pos` states that for any type `α` that has multiplication and one as a unit, zero, and a preorder relation, and additionally satisfies strict monotonicity of multiplication by positive elements on the left, if a value `a` in `α` is less than or equal to one, `b` is less than one, and `a` is greater than zero, then the product `a * b` is less than one. This theorem assumes left covariance.
More concisely: If `α` is a type with multiplication, one as a unit, zero, preorder relation, and left-strictly monotonic multiplication by positive elements, then `a <= 1`, `b < 1`, and `0 < a` imply `a * b < 1`.
|
lt_of_mul_lt_mul_of_nonneg_right
theorem lt_of_mul_lt_mul_of_nonneg_right :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : MulPosReflectLT α],
b * a < c * a → 0 ≤ a → b < c
This theorem, referred to as an alias of `lt_of_mul_lt_mul_right`, states that for any type `α` that supports multiplication, zero, a preorder, and satisfies the property of strict reverse monotonicity of multiplication by nonnegative elements on the right, if the product of `b` and `a` is less than the product of `c` and `a` and `a` is nonnegative, then `b` is less than `c`. In simpler terms, if `b * a < c * a` and `a ≥ 0`, then `b < c`. This theorem is a key result in the theory of ordered rings and semirings.
More concisely: If `α` is a type with multiplication, zero, a preorder, and strict reverse monotonicity of multiplication by nonnegative elements on the right, then `b < c` whenever `b * a < c * a` and `a ≥ 0`.
|
Mathlib.Algebra.Order.Ring.Lemmas._auxLemma.5
theorem Mathlib.Algebra.Order.Ring.Lemmas._auxLemma.5 :
∀ {α : Type u_1} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulStrictMono α]
[inst_3 : PosMulReflectLT α], 0 < a → (0 < a * b) = (0 < b)
The theorem `Mathlib.Algebra.Order.Ring.Lemmas._auxLemma.5` in Lean 4 states that for any type `α` equipped with a multiplication operation, a zero element, and a preorder relation, and if this type `α` satisfies two properties: strict monotonicity of multiplication by positive elements on the left (`PosMulStrictMono α`) and strict reverse monotonicity of multiplication by nonnegative elements on the left (`PosMulReflectLT α`), then for any two elements `a` and `b` from `α`, if `a` is positive (i.e., `0 < a`), then `a` times `b` is positive if and only if `b` is positive. In other words, it states that if `0 < a`, then `0 < a * b` is equivalent to `0 < b`.
More concisely: If `α` is a type with multiplication, zero, and preorder such that multiplication by positive elements is strictly monotonic and multiplication by nonnegative elements is strictly reverse monotonic, then for all `a, b ∈ α` with `0 < a`, we have `0 < a * b` if and only if `0 < b`.
|
pos_of_mul_pos_right
theorem pos_of_mul_pos_right :
∀ {α : Type u_1} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulReflectLT α],
0 < a * b → 0 ≤ a → 0 < b
The theorem `pos_of_mul_pos_right` states that for any type `α` that has a multiplication operation, zero element, and a preordering relation, and such that multiplication by nonnegative elements is strictly reverse monotonic on the left, if the product of two elements `a` and `b` is positive and `a` is nonnegative, then `b` must be positive. In simpler terms, it says that if you multiply a nonnegative number by another number and the result is positive, then the second number must be positive.
More concisely: If `α` is a type with multiplication, zero, preordering, and left-reverse monotonic multiplication by nonnegative elements, then `a * b > 0` implies `b > 0` when `a ≥ 0`.
|
Left.mul_pos
theorem Left.mul_pos :
∀ {α : Type u_1} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulStrictMono α],
0 < a → 0 < b → 0 < a * b
This theorem, `Left.mul_pos`, states that for any type `α` that has multiplication and zero, and is ordered with a strict monotonicity property under multiplication from the left by positive elements, if `a` and `b` are positive elements of `α` (i.e., `0 < a` and `0 < b`), then their product `a * b` is also positive (`0 < a * b`). The strict monotonicity property here is that if `b₁ < b₂` then `a * b₁ < a * b₂` for any `a > 0`. This theorem essentially asserts the positivity preservation property of multiplication in such a structure.
More concisely: If `α` is an ordered type with strict monotonic multiplication from the left by positive elements, then for any positive elements `a` and `b` in `α`, their product `a * b` is also positive.
|
Left.one_le_mul_of_le_of_le
theorem Left.one_le_mul_of_le_of_le :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : PosMulMono α],
1 ≤ a → 1 ≤ b → 0 ≤ a → 1 ≤ a * b
This theorem, named `Left.one_le_mul_of_le_of_le`, states that for any type `α` equipped with multiplication (`MulOneClass α`), zero (`Zero α`), and a preorder (`Preorder α`), and for any elements `a` and `b` of `α` that satisfy the property of monotonicity of multiplication by nonnegative elements on the left (`PosMulMono α`), if `1` is less than or equal to `a` and `b`, and `a` is nonnegative (i.e., greater than or equal to `0`), then `1` is less than or equal to the product of `a` and `b`. In terms of mathematical notation, it asserts that if $1 \leq a$, $1 \leq b$, and $0 \leq a$, then $1 \leq a \cdot b$.
More concisely: If `α` is a type with multiplication, zero, and a preorder, and `1 ≤ a`, `1 ≤ b`, and `0 ≤ a` hold in `α` with monotonicity of multiplication by nonnegative elements on the left, then `1 ≤ a * b`.
|
le_of_mul_le_mul_of_pos_right
theorem le_of_mul_le_mul_of_pos_right :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : MulPosReflectLE α],
b * a ≤ c * a → 0 < a → b ≤ c
The theorem `le_of_mul_le_mul_of_pos_right` is an alias for `le_of_mul_le_mul_right`. It states that for any type `α` that supports multiplication and a zero element and has a preorder and satisfies the property of reverse monotonicity of multiplication by positive elements on the right (i.e., MulPosReflectLE), given three elements `a`, `b`, and `c` of this type, if the product of `b` and `a` is less than or equal to the product of `c` and `a`, and `a` is positive (i.e., greater than zero), then `b` is less than or equal to `c`. In mathematical terms, this theorem asserts that for all `a`, `b`, and `c`, if $ba \leq ca$ and $a > 0$, then $b \leq c$.
More concisely: If `α` is a type with preorder, supports multiplication and a zero element, and has reverse monotonic multiplication by positive elements on the right, then for all `a`, `b`, `c` of `α` with `a > 0` and `ba ≤ ca`, it follows that `b ≤ c`.
|
mul_le_mul_iff_of_pos_left
theorem mul_le_mul_iff_of_pos_left :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : PosMulMono α]
[inst_4 : PosMulReflectLE α], 0 < a → (a * b ≤ a * c ↔ b ≤ c)
The theorem `mul_le_mul_iff_of_pos_left` states that for any type `α` which supports multiplication, zero, and has a preorder structure, and in addition supports monotonic multiplication by nonnegative elements on the left (i.e., `b₁ ≤ b₂ → a * b₁ ≤ a * b₂` if `0 ≤ a`), as well as reverse monotonicity of multiplication by positive elements on the left (i.e., `a * b₁ ≤ a * b₂ → b₁ ≤ b₂` if `0 < a`), then for all `a`, `b`, and `c` of type `α`, if `a` is positive, the inequality `a * b ≤ a * c` holds if and only if `b ≤ c`. This theorem is a key property of ordered semirings and linear ordered semirings.
More concisely: For any type `α` with multiplication, zero, preorder structure, and monotonic left multiplication by nonnegative elements and reverse monotonic left multiplication by positive elements, if `a` is positive in `α`, then `a * b ≤ a * c` if and only if `b ≤ c`.
|
Left.mul_le_one_of_le_of_le
theorem Left.mul_le_one_of_le_of_le :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : PosMulMono α],
a ≤ 1 → b ≤ 1 → 0 ≤ a → a * b ≤ 1
The theorem `Left.mul_le_one_of_le_of_le` states that for any type `α` equipped with instances for multiplication by one (`MulOneClass`), a zero element (`Zero`), a preorder structure (`Preorder`), and monotonicity of multiplication by nonnegative elements on the left (`PosMulMono`), if `a` and `b` are elements of `α` such that `a` and `b` are both less than or equal to 1 and `a` is nonnegative, then the product `a * b` is also less than or equal to 1. This theorem essentially formalizes the property that the product of two numbers, both less than or equal to 1 and one of them nonnegative, is still less than or equal to 1.
More concisely: For any type `α` with `MulOneClass`, `Zero`, `Preorder`, and `PosMulMono instances, if `a` and `b` are elements of `α` such that `0 ≤ a ≤ 1` and `0 ≤ b ≤ 1`, then `a * b ≤ 1`.
|
mul_self_le_mul_self
theorem mul_self_le_mul_self :
∀ {α : Type u_1} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulMono α]
[inst_3 : MulPosMono α], 0 ≤ a → a ≤ b → a * a ≤ b * b
The theorem `mul_self_le_mul_self` states that for any type `α` equipped with multiplication and zero (`MulZeroClass`), a preorder relation (`Preorder`), and the properties of left and right monotonicity of multiplication by nonnegative elements (`PosMulMono` and `MulPosMono`), if `a` and `b` are two elements of `α` such that `0 ≤ a` and `a ≤ b`, then it must be the case that `a * a ≤ b * b`. This is essentially stating a property of nonnegative real numbers that if `a` is less than or equal to `b` then `a` squared is also less than or equal to `b` squared, generalized to any ordered semiring structure.
More concisely: If `α` is an ordered semiring with multiplication and zero, and `a`, `b` in `α` satisfy `0 ≤ a ≤ b`, then `a * a ≤ b * b`.
|
Left.one_lt_mul_of_le_of_lt_of_pos
theorem Left.one_lt_mul_of_le_of_lt_of_pos :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α]
[inst_3 : PosMulStrictMono α], 1 ≤ a → 1 < b → 0 < a → 1 < a * b
This theorem, `Left.one_lt_mul_of_le_of_lt_of_pos`, states that for any type `α` equipped with a multiplication operation, a multiplicative identity (`1`), a zero element, and a preorder relation, if the type `α` also satisfies the property of strict monotonicity of multiplication by positive elements on the left (defined by the `PosMulStrictMono α` typeclass), then for any elements `a` and `b` of this type, if `1` is less than or equal to `a`, `1` is less than `b`, and `a` is positive (greater than `0`), then the product of `a` and `b` is greater than `1`. In other words, if we are dealing with an ordered structure where multiplication by a positive element is strictly increasing, then the product of a number that is at least `1` and a number that is greater than `1` is also greater than `1`, as long as the first number is positive.
More concisely: Given a type `α` with multiplication, a multiplicative identity `1`, a zero element, a preorder relation, and `PosMulStrictMono` property, if `1` is less than both `a` and `b`, and `a` is positive, then `a * b` is greater than `1`.
|
mul_pos_iff_of_pos_left
theorem mul_pos_iff_of_pos_left :
∀ {α : Type u_1} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulStrictMono α]
[inst_3 : PosMulReflectLT α], 0 < a → (0 < a * b ↔ 0 < b)
The theorem `mul_pos_iff_of_pos_left` states that for any type `α` with multiplication and zero properties, and strict monotonicity and reverse monotonicity of multiplication by positive and nonnegative elements (respectively), if `a` is a positive element of `α`, then the product `a * b` is positive if and only if `b` is positive. In other words, the positivity of the product `a * b` depends solely on the positivity of `b` when `a` is positive.
More concisely: For any type `α` with multiplication and zero, and strictly monotonic multiplication by positive elements and reverse monotonic multiplication by nonnegative elements, a positive element `a` of `α` implies `a * b` is positive if and only if `b` is positive.
|
mul_le_mul_iff_of_pos_right
theorem mul_le_mul_iff_of_pos_right :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : MulPosMono α]
[inst_4 : MulPosReflectLE α], 0 < a → (b * a ≤ c * a ↔ b ≤ c)
This theorem, `mul_le_mul_iff_of_pos_right`, is an alias of `mul_le_mul_right`. It takes as inputs a type `α`, three elements `a`, `b`, `c` of this type, and four instances that `α` is a multiplicative structure, a zero-structure, a preordered structure, has the property `MulPosMono`, and has the property `MulPosReflectLE`. The theorem states that if `a` is greater than zero, then the inequality `b * a ≤ c * a` holds if and only if `b ≤ c`. In other words, for positive `a`, multiplication by `a` on the right preserves the order of `b` and `c`.
More concisely: For all types `α` with the given instances and for all `a, b, c` of type `α` with `a > 0`, `b ≤ c` if and only if `b * a ≤ c * a`.
|
mul_lt_of_lt_one_left
theorem mul_lt_of_lt_one_left :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α]
[inst_3 : MulPosStrictMono α], 0 < b → a < 1 → a * b < b
The theorem `mul_lt_of_lt_one_left` states that for any type `α` that supports multiplication, has a multiplicative identity, has a zero, and is a preorder (i.e., supports at least a binary relation that is reflexive and transitive), and moreover obeys the property of strict monotonicity of multiplication by positive elements, then for any two elements `a` and `b` of this type, if `b` is positive and `a` is less than the multiplicative identity (1), then `a * b` is less than `b`.
More concisely: If `α` is a preorder type with multiplication, identity, zero, and strict monotonicity by positive elements, then for all `a` less than the identity and `b` positive in `α`, `a * b` is less than `b`.
|
Left.mul_nonneg
theorem Left.mul_nonneg :
∀ {α : Type u_1} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulMono α],
0 ≤ a → 0 ≤ b → 0 ≤ a * b
The theorem `Left.mul_nonneg` states that for any type `α` equipped with a multiplication operation, a zero element, and a preorder relation, and for any two elements `a` and `b` of `α`, if the multiplication operation of `α` is left-monotonic (meaning, a positive or zero multiplier always results in larger or equal result), then if both `a` and `b` are non-negative (i.e., greater than or equal to zero), their product `a * b` is also non-negative. This theorem is essentially asserting the non-negativity preserving nature of multiplication under the conditions of the multiplication being left-monotonic and the operands being non-negative.
More concisely: If `α` is a type with a left-monotonic multiplication operation, a zero element, and a preorder relation, then for all non-negative elements `a` and `b` in `α`, their product `a * b` is non-negative.
|
mul_le_mul_right
theorem mul_le_mul_right :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : MulPosMono α]
[inst_4 : MulPosReflectLE α], 0 < a → (b * a ≤ c * a ↔ b ≤ c)
The theorem `mul_le_mul_right` states that for any type `α` that supports multiplication and zero, and has a preorder structure, and satisfies the properties of multiplication positivity monotonicity and multiplication positivity reflectivity, if `a` is a positive element of `α`, then the product of `b` and `a` is less than or equal to the product of `c` and `a` if and only if `b` is less than or equal to `c`. This theorem is basically saying that multiplying by a positive value on the right preserves the order of elements.
More concisely: For any type `α` with multiplication, zero, preorder structure, and multiplication positivity monotonicity and reflectivity properties, if `a` is positive and `b ≤ c`, then `b * a ≤ c * a`.
|
mul_lt_mul_iff_of_pos_right
theorem mul_lt_mul_iff_of_pos_right :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : MulPosStrictMono α]
[inst_4 : MulPosReflectLT α], 0 < a → (b * a < c * a ↔ b < c)
The theorem `mul_lt_mul_iff_of_pos_right` states that given a type `α` equipped with operations of multiplication and zero, and an order relation that satisfies the properties of pre-ordered set, strict monotonicity of multiplication by positive elements on the right, and strict reverse monotonicity of multiplication by nonnegative elements on the right, if `a` is a positive element of type `α`, then the inequality `b * a < c * a` holds if and only if `b < c`. This theorem essentially asserts that multiplying both sides of an inequality by a positive element does not alter the order relation.
More concisely: Given a preordered type with multiplication and a positive element `a`, the inequality `b < c` is equivalent to `b * a < c * a`.
|
Right.mul_pos
theorem Right.mul_pos :
∀ {α : Type u_1} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : MulPosStrictMono α],
0 < a → 0 < b → 0 < a * b
The theorem `Right.mul_pos` states that for any type `α` that has multiplication and zero defined on it, and where multiplication by positive elements on the right is strictly increasing, and also has a preorder defined on it, if `a` and `b` are elements of `α` and both `a` and `b` are positive (i.e., greater than zero), then the product `a * b` is also positive. This theorem assumes right covariance, meaning the multiplication operation has the property that, if one factor increases, the product increases as well.
More concisely: If `α` is a type with multiplication, zero, preorder, and right-strictly increasing multiplication by positive elements, then for all positive `a` and `b` in `α`, their product `a * b` is also positive.
|
lt_mul_of_one_lt_left
theorem lt_mul_of_one_lt_left :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α]
[inst_3 : MulPosStrictMono α], 0 < b → 1 < a → b < a * b
The theorem `lt_mul_of_one_lt_left` states that for any type `α` that has multiplication and a one element (`MulOneClass α`), a zero element (`Zero α`), and a preorder comparison (`Preorder α`), and also satisfies the property of strict monotonicity of multiplication by positive elements on the right (`MulPosStrictMono α`), if `b` is positive (`0 < b`) and `a` is greater than one (`1 < a`), then `b` is less than the product of `a` and `b` (`b < a * b`). In other words, if we have a strictly ordered semiring, and `b` is a positive element and `a` is an element greater than one, then the product of `a` and `b` is strictly greater than `b`.
More concisely: If `α` is a strictly ordered semiring with one element `1`, and `0 < a` and `0 < b`, then `b < a * b`.
|
mul_le_mul_of_nonneg_left
theorem mul_le_mul_of_nonneg_left :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : PosMulMono α],
b ≤ c → 0 ≤ a → a * b ≤ a * c
This theorem states that for any type `α` that has multiplication and zero defined on it, and is preordered, and has the property of `PosMulMono`, for any three elements `a`, `b`, and `c` of `α`, if `b` is less than or equal to `c` and `a` is nonnegative (i.e., `a` is greater than or equal to zero), then the product of `a` and `b` is less than or equal to the product of `a` and `c`. This is the principle of monotonicity of multiplication by nonnegative elements on the left.
More concisely: For any preordered type `α` with multiplication and zero, if `a` is nonnegative and `b` is less than or equal to `c`, then `a * b` is less than or equal to `a * c`.
|
Right.one_le_mul_of_le_of_le
theorem Right.one_le_mul_of_le_of_le :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : MulPosMono α],
1 ≤ a → 1 ≤ b → 0 ≤ b → 1 ≤ a * b
This theorem, `Right.one_le_mul_of_le_of_le`, states that given a certain type `α` that satisfies the properties of having a multiplication operation (`MulOneClass`), a zero element (`Zero`), an order relation (`Preorder`), and where multiplication by nonnegative elements on the right is monotonic (`MulPosMono`), if two elements `a` and `b` of this type are both greater than or equal to `1` and `b` is nonnegative, then the product of `a` and `b` is also greater than or equal to `1`.
More concisely: Given a type `α` with multiplication operation `Mul` that satisfies `MulOneClass`, `Zero`, `Preorder`, and `MulPosMono`, if `a` and `b` in `α` are both greater than or equal to 1 and `b` is nonnegative, then `a * b` is greater than or equal to 1.
|
Right.mul_le_one_of_le_of_le
theorem Right.mul_le_one_of_le_of_le :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : MulPosMono α],
a ≤ 1 → b ≤ 1 → 0 ≤ b → a * b ≤ 1
This theorem, named `Right.mul_le_one_of_le_of_le`, states that for any type `α` equipped with multiplication, an identity element for multiplication, a zero element, and a preorder relation, and satisfying the property of being monotonic with respect to multiplication by nonnegative elements on the right, if we have two elements `a` and `b` of `α` for which `a` and `b` are both less than or equal to `1` and `b` is nonnegative, then the product `a * b` is also less than or equal to `1`. This essentially means that in such a mathematical structure, multiplication of two elements that are less than or equal to `1` will result in an output that is also less than or equal to `1`.
More concisely: If `α` is a type with multiplication, an identity element, a zero element, and a preorder relation such that multiplication by nonnegative elements is monotonic on the right, then for all `a`, `b` in `α` with `a`, `b ≤ 1` and `b ≥ 0`, we have `a * b ≤ 1`.
|
le_mul_iff_one_le_left
theorem le_mul_iff_one_le_left :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : MulPosMono α]
[inst_4 : MulPosReflectLE α], 0 < a → (a ≤ b * a ↔ 1 ≤ b)
The theorem `le_mul_iff_one_le_left` states that for any type `α` equipped with multiplication, zero, and a preorder, and where multiplication is both monotonically increasing when multiplying by nonnegative elements on the right (`MulPosMono`) and has reverse monotonicity when multiplying by positive elements on the right (`MulPosReflectLE`), if `a` is a positive element, then `a` is less than or equal to `b * a` if and only if `1` is less than or equal to `b`.
More concisely: For any type equipped with multiplication, zero, and a preorder such that multiplication by nonnegative elements on the right is monotonically increasing and has reverse monotonicity with positive elements, if `a` is positive, then `a ≤ b * a` if and only if `1 ≤ b`.
|
mul_le_mul_left
theorem mul_le_mul_left :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : PosMulMono α]
[inst_4 : PosMulReflectLE α], 0 < a → (a * b ≤ a * c ↔ b ≤ c)
The theorem `mul_le_mul_left` states that for any type `α` equipped with multiplication, zero element, and a preorder structure, and satisfying both the properties of `PosMulMono` and `PosMulReflectLE`, whenever `a` is a positive element of `α`, the inequality `a * b ≤ a * c` holds if and only if `b ≤ c`. In other words, multiplication by a positive element on the left preserves the order of elements. This property is commonly known in the context of ordered semirings or ordered fields.
More concisely: For any type `α` with multiplication, zero element, preorder structure, and satisfying `PosMulMono` and `PosMulReflectLE` properties, multiplication by a positive element on the left preserves the order relation: `a > 0 ∧ b ≤ c ↔ a * b ≤ a * c`.
|
lt_mul_of_one_lt_right
theorem lt_mul_of_one_lt_right :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α]
[inst_3 : PosMulStrictMono α], 0 < a → 1 < b → a < a * b
The theorem `lt_mul_of_one_lt_right` states that for any type `α` that has a multiplication operation, a multiplicative identity (one), a zero, and a preorder relation (a binary relation that is reflexive and transitive), and also obeys the property of strict monotonicity of multiplication by positive elements on the left, if we have two elements `a` and `b` of this type such that `a` is positive and `b` is greater than the multiplicative identity, then `a` is less than the product of `a` and `b`. In simpler terms, if `a` is a positive number and `b` is greater than one, then `a` is less than `a * b`.
More concisely: For any type with a multiplication operation, multiplicative identity, zero, preorder relation, and strict monotonicity of left multiplication by positives, if `a` is positive and `b` is greater than the identity, then `a` is strictly less than `a * b`.
|
mul_neg_of_pos_of_neg
theorem mul_neg_of_pos_of_neg :
∀ {α : Type u_1} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulStrictMono α],
0 < a → b < 0 → a * b < 0
The theorem `mul_neg_of_pos_of_neg` states that for all types `α` that are instances of a multiplication-zero class, have a preorder relation, and satisfy the property of strict monotonicity of multiplication by positive elements on the left, if `a` is a positive element and `b` is a negative element, then the product of `a` and `b` is a negative element. In other words, if `0 < a` and `b < 0`, then `a * b < 0`. This corresponds to the standard rule in mathematics that the product of a positive and a negative number is always negative.
More concisely: If `α` is a type with multiplication and zero, and `0 < a` and `b < 0`, then `a * b < 0`.
|
mul_lt_mul_of_pos_right
theorem mul_lt_mul_of_pos_right :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : MulPosStrictMono α],
b < c → 0 < a → b * a < c * a
The theorem `mul_lt_mul_of_pos_right` states that for any type `α` which has multiplication (`Mul α`), zero (`Zero α`), has a preorder relation (`Preorder α`), and satisfies strict monotonicity for multiplication by positive elements on the right (`MulPosStrictMono α`), if `b` is less than `c` and `a` is positive, then the product of `b` and `a` is less than the product of `c` and `a`. In mathematical terms, this can be written as: if `b < c` and `0 < a`, then `b * a < c * a`.
More concisely: If `α` has multiplication, zero, a preorder relation, and multiplication is strictly monotonic on the right for positive elements, then for any `a positive in α` and `b, c in α` with `b < c`, it holds that `b * a < c * a`.
|
Right.mul_nonneg
theorem Right.mul_nonneg :
∀ {α : Type u_1} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : MulPosMono α],
0 ≤ a → 0 ≤ b → 0 ≤ a * b
This theorem, named `Right.mul_nonneg`, states a property about multiplication in the context of ordered semirings. Given any type `α` that is an instance of a `MulZeroClass` (i.e., it supports multiplication and has a zero element), a `Preorder` (i.e., it supports an order which is reflexive and transitive), and `MulPosMono` (i.e., it is monotonic for multiplication by nonnegative elements), the theorem asserts that if two elements `a` and `b` of this type are both nonnegative (i.e., `0 ≤ a` and `0 ≤ b`), then their product is also nonnegative (i.e., `0 ≤ a * b`).
More concisely: In an ordered semiring where multiplication is monotonic for nonnegative elements, the product of two nonnegative elements is nonnegative.
|
mul_pos_iff_of_pos_right
theorem mul_pos_iff_of_pos_right :
∀ {α : Type u_1} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : MulPosStrictMono α]
[inst_3 : MulPosReflectLT α], 0 < b → (0 < a * b ↔ 0 < a)
The theorem `mul_pos_iff_of_pos_right` states that for any type `α` equipped with multiplication and zero, and any elements `a` and `b` of `α`, under the conditions that `α` has a multiplication-zero structure (`MulZeroClass`), a preorder structure, follows the strict monotonicity of multiplication by positive elements on the right (`MulPosStrictMono`), and the strict reverse monotonicity of multiplication by nonnegative elements on the right (`MulPosReflectLT`), then if `b` is strictly positive, the product `a * b` is strictly positive if and only if `a` is strictly positive. This theorem basically provides a criterion for determining whether a number is positive based on the positivity of its product with another positive number.
More concisely: Given a type `α` with multiplication and zero, and assuming `α` has a multiplication-zero structure, a preorder, multiplication is strict monotonic on the right by positive elements, and multiplication is strict reverse monotonic on the left by nonnegative elements, then `a * b` is strictly positive if and only if `a` is strictly positive, for all `a, b` in `α` with `b` strictly positive.
|
lt_of_mul_lt_mul_left
theorem lt_of_mul_lt_mul_left :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : PosMulReflectLT α],
a * b < a * c → 0 ≤ a → b < c
This theorem states that for any type `α` equipped with multiplication, zero, and a preorder relation where multiplication by nonnegative elements on the left is strictly reverse monotone, if the product of `a` and `b` is less than the product of `a` and `c` and `a` is nonnegative, then `b` is less than `c`. In mathematical terms, given `0 ≤ a` and `a * b < a * c`, it concludes `b < c`. This is a property related to the ordering of elements in the context of a linear ordered semiring.
More concisely: If `α` is a linear ordered semiring with non-negative `a`, `b`, and `c`, then `a * b < a * c` implies `b < c`.
|
Right.one_lt_mul_of_le_of_lt_of_nonneg
theorem Right.one_lt_mul_of_le_of_lt_of_nonneg :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : MulPosMono α],
1 ≤ a → 1 < b → 0 ≤ b → 1 < a * b
The theorem `Right.one_lt_mul_of_le_of_lt_of_nonneg` states that for any type `α` with instances of multiplication and one, zero, and a preorder relation, and also assuming multiplication is monotonic for non-negative elements, if we have two elements `a` and `b` in `α` where `a` is at least `1`, `b` is strictly greater than `1` and `b` is also non-negative, then the product of `a` and `b` will be strictly greater than `1`.
More concisely: If `α` is a type with multiplication, one, zero, and a preorder relation, and multiplication is monotonic for non-negative elements, then for all `a : α` with `a >= 1` and `b : α` with `b > 1` and `b >= 0`, we have `a * b > 1`.
|
mul_pos
theorem mul_pos :
∀ {α : Type u_1} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulStrictMono α],
0 < a → 0 < b → 0 < a * b
The theorem `mul_pos` is an alias of `Left.mul_pos` and it assumes left covariance. The theorem is defined for any type `α` that has a multiplication operation, a zero element, and a strict preorder relation, and the multiplication operation should strictly increase when you multiply by a positive element on the left side. If `a` and `b` are elements of the type `α` and both `a` and `b` are greater than zero, then the product `a * b` is also greater than zero.
More concisely: If `α` is a type with multiplication, zero, and a strict preorder such that `a * b` strictly increases with positive elements on the left, then for all positive elements `a` and `b` in `α`, `a * b` is also positive.
|
mul_neg_of_neg_of_pos
theorem mul_neg_of_neg_of_pos :
∀ {α : Type u_1} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : MulPosStrictMono α],
a < 0 → 0 < b → a * b < 0
The theorem `mul_neg_of_neg_of_pos` states that, for any type `α` that is a multiplication zero class (`MulZeroClass`), has a preorder, and satisfies the property of strict monotonicity of multiplication by positive elements (`MulPosStrictMono`), if `a` is less than zero and `b` is greater than zero, then the product of `a` and `b` is less than zero. In other words, it states that multiplying a negative number by a positive number results in a negative number, under the conditions specified by the typeclasses involved.
More concisely: If `α` is a type with multiplication, zero, preorder, and strict monotonicity properties such that `a` is negative and `b` is positive, then `a * b` is negative.
|
mul_lt_mul_of_pos_left
theorem mul_lt_mul_of_pos_left :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : PosMulStrictMono α],
b < c → 0 < a → a * b < a * c
The theorem `mul_lt_mul_of_pos_left` states that for any type `α` that has multiplication (`Mul α`), zero element (`Zero α`), a preorder structure (`Preorder α`) and obeys the principle of strict monotonicity of multiplication by positive elements on the left (`PosMulStrictMono α`), if `b` is less than `c` and `a` is positive, then the product of `a` and `b` is strictly less than the product of `a` and `c`. In other words, if `b < c` and `0 < a`, then `a * b < a * c`. This is a property of ordered rings where the multiplication of a smaller number with a positive number results in a smaller product.
More concisely: If `α` is an ordered ring with multiplication, zero, preorder, and strict monotonicity of multiplication by positive elements on the left, then for any positive `a` and `b` with `b` less than `c`, `a * b` is strictly less than `a * c`.
|
mul_lt_mul_right
theorem mul_lt_mul_right :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : MulPosStrictMono α]
[inst_4 : MulPosReflectLT α], 0 < a → (b * a < c * a ↔ b < c)
The theorem `mul_lt_mul_right` states that for any strictly ordered semiring `α`, given three elements `a`, `b`, and `c` of `α`, if `a` is positive, then `b * a` is less than `c * a` if and only if `b` is less than `c`. This theorem asserts the property of preserving order under multiplication by a positive element on the right, and that the order can be reflected through the same operation. This is a characteristic property of strict ordered semirings.
More concisely: In a strictly ordered semiring, for all positive elements `a`, `b`, and `c`, `b < c` if and only if `b * a < c * a`.
|
lt_of_mul_lt_mul_right
theorem lt_of_mul_lt_mul_right :
∀ {α : Type u_1} {a b c : α} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : MulPosReflectLT α],
b * a < c * a → 0 ≤ a → b < c
This theorem states that for any type `α` that has a multiplication operation, a zero element, a preorder relation, and satisfies the property of strict reverse monotonicity of multiplication by nonnegative elements on the right (denoted as `MulPosReflectLT α`), if the product of `b` and `a` is less than the product of `c` and `a` and `a` is nonnegative (zero or positive), then `b` is less than `c`. In other words, for all nonnegative `a`, if `b * a < c * a`, then `b < c`. This is a manifestation of the characteristic property of order-preserving (or reversing) by multiplication in ordered semirings or related algebraic structures.
More concisely: For any type `α` with multiplication, zero, preorder relation, and `MulPosReflectLT`, if `a` is nonnegative and `b * a < c * a`, then `b < c`.
|
mul_le_of_le_one_left
theorem mul_le_of_le_one_left :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : MulPosMono α],
0 ≤ b → a ≤ 1 → a * b ≤ b
This theorem states that for any type 'α' equipped with multiplication, one, zero, and a preorder relation, which also satisfies the property of positive monotonicity of multiplication, if 'b' is a nonnegative element ('b' is greater than or equal to zero), and 'a' is less than or equal to one, then the product of 'a' and 'b' is less than or equal to 'b'. In mathematical terms, if 0 ≤ b and a ≤ 1, then a*b ≤ b. This theorem thus captures a property of multiplication specific to partially ordered algebraic structures, where multiplication by an element less than or equal to one does not increase the magnitude of another nonnegative element.
More concisely: For any type 'α' with multiplication, one, zero, and a preorder relation satisfying positive monotonicity, if 0 ≤ b and 0 ≤ a, then a * b ≤ b.
|
le_mul_of_one_le_right
theorem le_mul_of_one_le_right :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α] [inst_3 : PosMulMono α],
0 ≤ a → 1 ≤ b → a ≤ a * b
This theorem states that for any type `α` that has multiplication and one as a multiplicative identity (i.e., it is a `MulOneClass`), is ordered (i.e., it has a `Preorder`, meaning it has a less than or equal to relation that is reflexive and transitive), and multiplication by nonnegative elements is monotonically increasing (i.e., it has the `PosMulMono` property), if `a` and `b` are elements of `α` where `a` is nonnegative and `b` is at least one, then `a` is less than or equal to the product of `a` and `b`. In mathematical terms, the theorem says: if $0 \leq a$ and $1 \leq b$, then $a \leq a \cdot b$.
More concisely: If `α` is a type with multiplicative identity one, preorder, and monotonically increasing multiplication by nonnegative elements, then for all nonnegative `a` and `b` in `α` with `b` being at least one, we have `a ≤ a * b`.
|
mul_nonpos_of_nonneg_of_nonpos
theorem mul_nonpos_of_nonneg_of_nonpos :
∀ {α : Type u_1} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulMono α],
0 ≤ a → b ≤ 0 → a * b ≤ 0
This theorem states that for any type `α` that is a multiplication-zero class and has a preorder and positive multiplication monoticity property, if `a` and `b` are elements of `α` such that `a` is nonnegative (i.e., `0 ≤ a`) and `b` is nonpositive (i.e., `b ≤ 0`), then the product of `a` and `b` is nonpositive (i.e., `a * b ≤ 0`). In simpler terms, it states that the product of a nonnegative number and a nonpositive number is less than or equal to zero.
More concisely: For any multiplication-zero class `α` with preorder and positive multiplication monotonicity, `0 ≤ a` and `b ≤ 0` imply `a * b ≤ 0`.
|
Right.mul_lt_one_of_lt_of_le_of_pos
theorem Right.mul_lt_one_of_lt_of_le_of_pos :
∀ {α : Type u_1} {a b : α} [inst : MulOneClass α] [inst_1 : Zero α] [inst_2 : Preorder α]
[inst_3 : MulPosStrictMono α], a < 1 → b ≤ 1 → 0 < b → a * b < 1
This theorem, named `Right.mul_lt_one_of_lt_of_le_of_pos`, states that for any type `α` that has a multiplication and one, zero, and a preorder structure, and for which multiplication by positive elements is strictly monotonic on the right, if `a` is a value of type `α` that is less than 1, `b` is a value of type `α` that is less than or equal to 1, and `b` is strictly greater than zero, then the product of `a` and `b` will be less than 1. It encapsulates the mathematical idea that if you multiply a number less than 1 by another number that's positive and less than or equal to 1, the result is still less than 1.
More concisely: If `a` is a number less than 1, `b` is a positive number less than or equal to 1, then `a * b` is less than 1.
|
mul_nonneg
theorem mul_nonneg :
∀ {α : Type u_1} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulMono α],
0 ≤ a → 0 ≤ b → 0 ≤ a * b
The theorem `mul_nonneg` is an alias of `Left.mul_nonneg`. It states that for any type `α` with a multiplication operation, a zero element, and a preorder relation, and that satisfies the property of monotonicity of multiplication by nonnegative elements on the left (i.e., is a `PosMulMono`), if `a` and `b` are elements of `α` such that `0 ≤ a` and `0 ≤ b`, then it must be the case that `0 ≤ a * b`. In other words, the product of two nonnegative elements in such a type is also nonnegative. This theorem assumes left covariance.
More concisely: In a type with a monotonic multiplication by nonnegative elements on the left, the product of two nonnegative elements is nonnegative.
|