StrictAntiOn.mul_antitone'
theorem StrictAntiOn.mul_antitone' :
∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
[inst_3 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1],
StrictAntiOn f s → AntitoneOn g s → StrictAntiOn (fun x => f x * g x) s
The theorem `StrictAntiOn.mul_antitone'` states that for any given set `s` of a type `β`, if `f` and `g` are functions from `β` to a type `α` such that `f` is strictly antitone (strictly decreasing) on `s` and `g` is antitone (non-increasing) on `s`, then the product function `(f x) * (g x)` is also strictly antitone on `s`. Here, `α` is a type with a multiplication operation and the properties of a preorder (reflexivity and transitivity), while `β` is a type with a preorder. The theorem also assumes that `α` is a covariant class under both multiplication and its swapped version, which means that if `x ≤ y` then `x * z ≤ y * z` and if `x < y` then `z * x < z * y`.
More concisely: If `f` is strictly decreasing and `g` is non-increasing on a set `s` of a preordered type `β`, then their product `(f x) * (g x)` is strictly decreasing on `s`, assuming `α` is a preordered type with multiplication and the property that `x ≤ y` implies `x * z ≤ y * z` for all `x, y, z` in `α`.
|
AddLECancellable.add_le_add_iff_left
theorem AddLECancellable.add_le_add_iff_left :
∀ {α : Type u_1} [inst : LE α] [inst_1 : Add α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α},
AddLECancellable a → (a + b ≤ a + c ↔ b ≤ c)
The theorem `AddLECancellable.add_le_add_iff_left` states that for any type `α` equipped with an addition operation and a less than or equal to order relation, and for any elements `a`, `b`, `c` of that type, if `a` is `AddLECancellable` (meaning the function `x ↦ a + x` is order-reflecting or, in other words, for all `b` and `c`, if `a + b` is less than or equal to `a + c`, then `b` is less than or equal to `c`), then `a + b` is less than or equal to `a + c` if and only if `b` is less than or equal to `c`.
More concisely: For any AddLECancellable element `a` in a type with addition and order relation, `a + b` is less than or equal to `a + c` if and only if `b` is less than or equal to `c`.
|
Left.add_nonneg
theorem Left.add_nonneg :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, 0 ≤ a → 0 ≤ b → 0 ≤ a + b
This theorem, `Left.add_nonneg`, asserts that for any type `α` that has an addition operation with a zero element (captured by the `AddZeroClass`), a preorder relation (as captured by `Preorder`), and satisfies left covariance (as captured by `CovariantClass`), if `a` and `b` are elements of `α` such that both are nonnegative (i.e., greater than or equal to zero), then the sum of `a` and `b` is also nonnegative. This is a property of ordered additive structures where addition preserves the order. The corresponding lemma for right covariance is `Right.add_nonneg`.
More concisely: If `α` is an ordered additive structure, then for all non-negative elements `a` and `b` in `α`, the sum `a + b` is also non-negative.
|
Left.mul_lt_one_of_le_of_lt
theorem Left.mul_lt_one_of_le_of_lt :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b : α}, a ≤ 1 → b < 1 → a * b < 1
This theorem, `Left.mul_lt_one_of_le_of_lt`, states that for any type `α` with instances of `MulOneClass` and `Preorder`, and given a left covariance relationship, if we have two elements `a` and `b` of `α` such that `a` is less than or equal to 1 and `b` is less than 1, then the product of `a` and `b` is less than 1.
It essentially establishes that under certain conditions, the product of two elements, one of which is less than or equal to 1 and the other less than 1, is always less than 1. The lemma for the corresponding scenario with right covariance is `Right.mul_lt_one_of_le_of_lt`.
More concisely: For types `α` with `MulOneClass` and `Preorder`, if `0 < a <= 1` and `0 < b`, then `a * b < 1`.
|
MulLECancellable.Injective
theorem MulLECancellable.Injective :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] {a : α},
MulLECancellable a → Function.Injective fun x => a * x
The theorem `MulLECancellable.Injective` states that for every type `α` that supports multiplication and has a partial order, and for any element `a` of that type, if `a` is `MulLECancellable` (meaning the function from `x` to `a * x` is order-reflecting), then the function that multiplies by `a` is injective (in other words, if `a * x = a * y` then `x = y`).
More concisely: If `α` is a type with multiplication and a partial order, and `a` in `α` is `MulLECancellable`, then the multiplication-by-`a` function is injective.
|
add_lt_add_iff_right
theorem add_lt_add_iff_right :
∀ {α : Type u_1} [inst : Add α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_3 : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b c : α},
b + a < c + a ↔ b < c
The theorem `add_lt_add_iff_right` states that, for a type `α` equipped with an addition operation and a less than operation, and satisfying certain covariance and contravariance properties (specifically, those asserting that addition behaves appropriately with respect to the order), adding a fixed element `a` from `α` to two other elements `b` and `c` from `α` yields a smaller value when `b` is less than `c`. More formally, it asserts that `b + a < c + a` if and only if `b < c`.
More concisely: For all types `α` with covariant and contravariant addition and a total order, if `a` is an element of `α` and `b` is less than `c`, then `b + a` is less than `c + a`. In other words, the order relation is preserved under addition.
|
lt_mul_of_one_lt_right'
theorem lt_mul_of_one_lt_right' :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] (a : α) {b : α}, 1 < b → a < a * b
This theorem, `lt_mul_of_one_lt_right'`, states that for any type `α` that has a multiplication operation and a less-than relation, and additionally the multiplication operation is covariant with respect to the less-than relation, for any two elements `a` and `b` of this type, if `b` is greater than 1, then `a` is less than the product of `a` and `b`. In simple terms, for any numbers `a` and `b`, if `b` is greater than 1, then `a` is less than `a` times `b`.
More concisely: For any type `α` with covariant multiplication and total order, if `1 < b` and `a < a * b`, then `a < 0` or `b > 1`. (Assuming Lean's negation of less-than relation `<` is defined as `>` in this context.)
|
StrictAnti.mul_antitone'
theorem StrictAnti.mul_antitone' :
∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α}
[inst_3 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1],
StrictAnti f → Antitone g → StrictAnti fun x => f x * g x
The theorem `StrictAnti.mul_antitone'` states that given two types `α` and `β` where `α` has a multiplication operation and both `α` and `β` have a preorder relation (that is, they are equipped with an order relation that is both reflexive and transitive), if `f` and `g` are functions from `β` to `α`, the product of a strictly antitone function `f` (a function where if `a < b` then `f(b) < f(a)`) and an antitone function `g` (a function where if `a ≤ b` then `f(b) ≤ f(a)`) is also a strictly antitone function. This statement assumes the existence of two CovariantClasses, which ensures that the multiplication operation on `α` respects the order relations.
More concisely: Given types `α` and `β` with multiplication and preorders, if `f` is strictly antitone and `g` is antitone, then the product function `x ↦ f(x) ⊤ g(x)` is strictly antitone, where `⊤` denotes function composition and preorders on `α` and `β` are covariant.
|
mul_lt_mul_right'
theorem mul_lt_mul_right' :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : LT α]
[i : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {b c : α},
b < c → ∀ (a : α), b * a < c * a
The theorem `mul_lt_mul_right'` states that for any type `α` that has a multiplication operation (`Mul α`) and a less than operation (`LT α`) and satisfies a certain covariance property, then given any three elements `a`, `b`, and `c` of `α` such that `b < c`, we have `b * a < c * a`. In other words, in this mathematical structure, if `b` is less than `c`, then multiplying `b` and `c` by the same factor `a` on the right maintains the inequality.
More concisely: For any type `α` with multiplication `(*`) and order `<`, if `b < c` then `b * a < c * a`.
|
StrictMono.mul'
theorem StrictMono.mul' :
∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α}
[inst_3 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1],
StrictMono f → StrictMono g → StrictMono fun x => f x * g x
This theorem states that if `f` and `g` are two strictly monotone functions, then their product function `(fun x => f x * g x)` is also strictly monotone. Here, strictly monotone means that for any two elements `a` and `b` in the domain, if `a` is less than `b`, then `f(a)` is less than `f(b)`. The conditions `CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1` and `CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1` are technical conditions which ensure that the multiplication operation in the codomain `α` is compatible with the order relation.
More concisely: If `f` and `g` are strictly monotone functions, then their product function `(fun x => f x * g x)` is also strictly monotone.
|
lt_add_of_pos_right
theorem lt_add_of_pos_right :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α}, 0 < b → a < a + b
This theorem, named `lt_add_of_pos_right`, states that for any type `α` equipped with an addition operation, a zero element, and a less-than relation such that addition is covariant with respect to the less-than relation, and for any elements `a` and `b` of this type, if `b` is greater than zero, then `a` is less than `a + b`. Simply put, adding a positive number to any number `a` results in a number greater than `a`.
More concisely: For any type equipped with a covariant addition, zero, and less-than relation, if `a` is an element and `b` is positive, then `a < a + b`.
|
Right.one_lt_mul'
theorem Right.one_lt_mul' :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α},
1 < a → 1 < b → 1 < a * b
The theorem `Right.one_lt_mul'` states that for any type `α` with a multiplication operation and also a preorder relation, and where the multiplication operation is right covariant with respect to the preorder relation, if `a` and `b` are elements of `α` such that both `a` and `b` are greater than 1, then their product `a * b` is also greater than 1. In mathematical terms, if we have `1 < a` and `1 < b`, then we also have `1 < a * b`. The corresponding theorem assuming left covariance is `Left.one_lt_mul'`.
More concisely: If `α` is a type with a multiplication operation and a preorder relation such that multiplication is right covariant with respect to the preorder, then `1 < a` and `1 < b` imply `1 < a * b`.
|
add_le_add_iff_left
theorem add_le_add_iff_left :
∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) {b c : α},
a + b ≤ a + c ↔ b ≤ c
This theorem, `add_le_add_iff_left`, states that for all types `α`, if `α` has addition (`Add α`) and an order relation (`LE α`) defined on it, and if it satisfies both covariant and contravariant properties under addition, then for any variable `a` of type `α`, and any two variables `b` and `c` of the same type, the inequality `a + b ≤ a + c` is equivalent to `b ≤ c`.
In mathematical terms, this might be stated as: "Given a type `α` under the conditions of addition and order, the addition of a common term `a` to both sides of an inequality does not change the inequality itself between `b` and `c`."
More concisely: For all types `α` with addition and order relations, `a + b ≤ a + c` if and only if `b ≤ c`.
|
Left.add_neg_of_neg_of_nonpos
theorem Left.add_neg_of_neg_of_nonpos :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, a < 0 → b ≤ 0 → a + b < 0
This theorem, titled `Left.add_neg_of_neg_of_nonpos`, states that given a type `α` that has an addition operation, a zero element, and a preorder relation, and is left-covariant, if an element `a` is less than zero and another element `b` is less than or equal to zero, then the sum of `a` and `b` is less than zero. The lemma assuming right covariance is `Right.add_neg_of_neg_of_nonpos`.
More concisely: If `α` is a type with an additive structure, a zero element, and a left-covariant preorder relation, then for all `a` less than zero and `b` less than or equal to zero, `a + b` is less than zero.
|
Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.4
theorem Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.4 :
∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) {b c : α},
(b + a ≤ c + a) = (b ≤ c)
This theorem is a statement about partially ordered additive monoids in the world of algebra. Given a type `α` which has an addition operation and a partial order defined on it, satisfying both covariant and contravariant properties with respect to addition, the theorem states that for any elements `a`, `b`, and `c` of this type, `b + a` is less than or equal to `c + a` if and only if `b` is less than or equal to `c`. This means that in such a structure, the inequality between `b` and `c` does not change when we add the same quantity `a` to both sides.
More concisely: For all types `α` with addition `+` and a partial order `≤` such that addition is covariant and contravariant with respect to the order, `b ≤ c` if and only if `b + a ≤ c + a` for all `a, b, c` in `α`.
|
Right.add_pos_of_pos_of_nonneg
theorem Right.add_pos_of_pos_of_nonneg :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α},
0 < a → 0 ≤ b → 0 < a + b
This theorem, `Right.add_pos_of_pos_of_nonneg`, is a statement about an ordered additive structure. It states that for any type `α` which has an addition operation and a zero element (`AddZeroClass`), and is equipped with an order (`Preorder`) that is right-covariant under addition (`CovariantClass` under the operation `Function.swap fun x x_1 => x + x_1`), if `a` and `b` are elements of `α` such that `a` is positive (greater than zero) and `b` is nonnegative (greater than or equal to zero), then the sum `a + b` is also positive. In other words, in this structure, adding a nonnegative number to a positive number results in a positive number.
More concisely: If `α` is an ordered additive structure with right-covariant order, where `a` is positive and `b` is nonnegative, then `a + b` is positive.
|
Right.one_le_mul
theorem Right.one_le_mul :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α},
1 ≤ a → 1 ≤ b → 1 ≤ a * b
This theorem, named `Right.one_le_mul`, states that for any type `α` that has a multiplication and unit element structure (`MulOneClass α`), a preorder relationship (`Preorder α`), and satisfies a right covariance property (`CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1`), if `a` and `b` are elements of `α` such that both `a` and `b` are greater than or equal to 1, then the product `a * b` is also greater than or equal to 1. The term "right covariance" refers to the property where multiplication on the right by an element always maps lesser elements to lesser or equal elements. This is a variant of the theorem where the covariance is assumed on the left, `Left.one_le_mul`.
More concisely: For any type `α` with a multiplication and unit element, preorder, and right covariance property, if `a` and `b` are elements greater than or equal to 1, then `a * b` is also greater than or equal to 1.
|
MonotoneOn.add_strictMono
theorem MonotoneOn.add_strictMono :
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {s : Set β}
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {f g : β → α},
MonotoneOn f s → StrictMonoOn g s → StrictMonoOn (fun x => f x + g x) s
The theorem `MonotoneOn.add_strictMono` states that for any set `s` of elements of some type `β`, if we have two functions `f` and `g` from `β` to `α` such that `f` is monotone on `s` and `g` is strictly monotone on `s`, then the function formed by the pointwise sum of `f` and `g` is strictly monotone on `s`. Here, monotonicity refers to the property that if `a` and `b` are elements of `s` and `a` is less than or equal to `b`, then `f(a)` is less than or equal to `f(b)`, and strict monotonicity refers to the property that if `a` is strictly less than `b`, then `g(a)` is strictly less than `g(b)`. The type `α` has a preorder and is equipped with an addition operation that is strictly increasing and non-decreasing when swapped.
More concisely: If `f` is monotone and `g` is strictly monotone on a set `s`, then the pointwise sum `f + g` is strictly monotone on `s`.
|
le_add_of_nonneg_left
theorem le_add_of_nonneg_left :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α},
0 ≤ b → a ≤ b + a
This theorem, `le_add_of_nonneg_left`, states that for any type `α` that has the structure of an `AddZeroClass` and a `LE` (less than or equal to) relation, and also satisfies the `CovariantClass` property with respect to addition (i.e., swapping the arguments of the addition function preserves the `LE` relation), if `a` and `b` are two elements of this type and `b` is nonnegative (meaning that `b` is greater than or equal to zero), then `a` is less than or equal to the sum of `b` and `a`. In mathematical terms, if `0 ≤ b`, then `a ≤ b + a`.
More concisely: If `α` is an AddZeroClass type with a Covariant LE relation such that `0 ≤ b`, then `a ≤ b + a`.
|
add_nonpos
theorem add_nonpos :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, a ≤ 0 → b ≤ 0 → a + b ≤ 0
The theorem `add_nonpos` states that for any type `α` that is an addition-zero class (meaning it has an addition operation and a zero), and that has a preorder (a relation that is reflexive and transitive), and is also a covariant class (where the addition operation and the preorder relation interact in a certain way), if `a` and `b` are elements of `α` such that `a` and `b` are both less than or equal to zero, then their sum `a + b` is also less than or equal to zero. In other words, the sum of two nonpositive elements is nonpositive.
More concisely: If `α` is an addition-zero class with a preorder and is covariant, then for all `a, b ∈ α` with `a ≤ 0` and `b ≤ 0`, we have `a + b ≤ 0`.
|
MonotoneOn.add
theorem MonotoneOn.add :
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
MonotoneOn f s → MonotoneOn g s → MonotoneOn (fun x => f x + g x) s
The theorem `MonotoneOn.add` states that for any two functions `f` and `g` defined on a set `s` of a certain type `β` with values in a type `α` that supports addition and has a preorder (a relation that is reflexive and transitive), if both `f` and `g` are monotone on `s` (meaning that for any two elements `a` and `b` in `s`, if `a` is less than or equal to `b`, then `f(a)` is less than or equal to `f(b)` and similarly for `g`), and if `α` satisfies two covariance conditions related to addition and the preorder relation, then the function defined by the sum of `f` and `g` (i.e., the function `x ↦ f(x) + g(x)`) is also monotone on `s`.
More concisely: If `f` and `g` are monotone functions on a preorder set `s` with values in an additive and preorder-covariant type `α`, then their pointwise sum is also a monotone function on `s`.
|
lt_add_of_pos_of_le
theorem lt_add_of_pos_of_le :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α},
0 < a → b ≤ c → b < a + c
This theorem, `lt_add_of_pos_of_le`, states that for any type `α` that is equipped with an addition operation, a zero element, and a preorder relation that respects the order of addition, if `a`, `b` and `c` are elements of this type such that `0 < a` and `b ≤ c`, then it must be the case that `b < a + c`. In other words, if `a` is positive and `b` is less than or equal to `c`, then `b` is strictly less than the sum of `a` and `c`.
More concisely: If `α` is a type with addition, zero, and a preorder relation such that `0 < a` and `b ≤ c` imply `b < a + c`, then this preorder relation is transitive on `α`. (This is an alternative way to state the theorem, emphasizing the transitivity property that results from it.)
|
AntitoneOn.mul_strictAnti'
theorem AntitoneOn.mul_strictAnti' :
∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {s : Set β}
[inst_3 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {f g : β → α},
AntitoneOn f s → StrictAntiOn g s → StrictAntiOn (fun x => f x * g x) s
This theorem states that for any type `α` with multiplication operation and preorder, and another type `β` also with preorder, given a set `s` of type `β`, if the binary operation '*' on type `α` is covariant in both arguments, then for any two functions `f` and `g` from `β` to `α`, if `f` is antitone on `s` (meaning for all elements `a` and `b` in `s`, if `a ≤ b`, then `f(b) ≤ f(a)`) and `g` is strictly antitone on `s` (meaning for all elements `a` and `b` in `s`, if `a < b`, then `g(b) < g(a)`), then the function that maps `x` to `f(x) * g(x)` is also strictly antitone on `s`.
More concisely: If `α` is a type with covariant multiplication and preorder, `β` is another type with preorder, `s` is a set of `β`, `f` is an antitone function from `s` to `α`, and `g` is a strictly antitone function from `s` to `α`, then the function `x ↦ f(x) * g(x)` is strictly antitone on `s`.
|
StrictAntiOn.add_antitone
theorem StrictAntiOn.add_antitone :
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1],
StrictAntiOn f s → AntitoneOn g s → StrictAntiOn (fun x => f x + g x) s
The theorem states that for a set `s` of type `β` and two functions `f` and `g` from `β` to `α`, if `f` is strictly antitone on `s` (meaning that for all `a` and `b` in `s`, `a < b` implies `f(b) < f(a)`) and `g` is antitone on `s` (meaning that for all `a` and `b` in `s`, `a ≤ b` implies `g(b) ≤ g(a)`), then the function that maps each element `x` in `s` to `f(x) + g(x)` is also strictly antitone on `s`. This is under the assumption that `α` supports addition and has a preorder relation, and the addition operation has certain covariance properties.
More concisely: If `f` is strictly antitone and `g` is antitone on a set `s`, then the function `x ↦ f(x) + g(x)` is strictly antitone on `s`, given that `α` is an additive and ordered semigroup with the property that `a + b ≤ c` implies `a ≤ a + b` and `b ≤ c`.
|
Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.19
theorem Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.19 :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α},
(a + b ≤ a) = (b ≤ 0)
This theorem, from the Mathlib library in the Algebra, Order, Monoid section, states that for any type `α` that has an `AddZeroClass` structure (meaning it has addition and zero element) and a lesser-than-or-equal-to (`LE`) order, and assuming that the addition operation is both covariant and contravariant (mathematical terms referring to how a function behaves under transformations), then for any elements `a` and `b` of `α`, `a + b` being less than or equal to `a` is equivalent to `b` being less than or equal to zero.
More concisely: For any type `α` with an `AddZeroClass` structure and an `LE` order, if addition is both covariant and contravariant, then `a + b <= a` if and only if `b <= 0`.
|
StrictMonoOn.add_monotone
theorem StrictMonoOn.add_monotone :
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1],
StrictMonoOn f s → MonotoneOn g s → StrictMonoOn (fun x => f x + g x) s
The theorem `StrictMonoOn.add_monotone` states that for any type `α` with addition and any preorder `β`, if `f` is a strictly monotone function and `g` is a monotone function both from `β` to `α` and defined on a set `s` of `β`, then the function that to each `x` in `s` assigns `f(x) + g(x)` is also strictly monotone on `s`. This holds under the conditions that `α` has a covariant class for addition with respect to the less or equal relation and a covariant class for swapped addition with respect to the less than relation.
More concisely: If `f` is strictly monotone and `g` is monotone, then the function `x ∈ s ↦ f(x) + g(x)` is strictly monotone on `s`, given `α` is an additive type with covariant classes for addition w.r.t. ≤ and swapped addition w.r.t. <.
|
Right.add_neg
theorem Right.add_neg :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α},
a < 0 → b < 0 → a + b < 0
The theorem `Right.add_neg` states that for any type `α` that has the structure of an additive zero class and is equipped with a preorder relation, and also satisfies the right covariance property with respect to addition and this preorder, if two elements `a` and `b` of this type are both less than zero, then their sum `a + b` is also less than zero. This theorem assumes right covariance, and there is a corresponding lemma `Left.add_neg` for the case where left covariance is assumed instead.
More concisely: For types equipped with an additive structure and a preorder relation satisfying right covariance, if two elements both have negative preorder values, then their sum has a negative preorder value as well.
|
Right.add_neg_of_nonpos_of_neg
theorem Right.add_neg_of_nonpos_of_neg :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α},
a ≤ 0 → b < 0 → a + b < 0
The theorem `Right.add_neg_of_nonpos_of_neg` states that for any type `α` that has an addition operation with a zero (`AddZeroClass α`), a preorder relation (`Preorder α`), and satisfies the property of right covariance (`CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1`), if `a` and `b` are elements of `α` such that `a` is less than or equal to zero and `b` is less than zero, then the sum of `a` and `b` is less than zero. This is assuming right covariance; there is a similar lemma for left covariance called `Left.add_neg_of_nonpos_of_neg`.
More concisely: If `α` is a type with AddZeroClass, Preorder, and right covariance, then for all `a, b ∈ α` with `a ≤ 0` and `b < 0`, we have `a + b < 0`.
|
lt_of_add_lt_add_left
theorem lt_of_add_lt_add_left :
∀ {α : Type u_1} [inst : Add α] [inst_1 : LT α]
[inst_2 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α},
a + b < a + c → b < c
This theorem, `lt_of_add_lt_add_left`, states that for any type `α` that has an addition operation, a less-than relation, and satisfies the contravariant property (i.e., adding something to both sides of a less-than comparison doesn't change the comparison), if `a + b` is less than `a + c`, then `b` is less than `c`. In other words, if adding the same value `a` to two quantities `b` and `c` results in a smaller sum for `b`, then `b` must have been smaller than `c` to begin with.
More concisely: If `α` is a type with addition and less-than relations satisfying the contravariant property, then `b < c` implies `a + b < a + c`.
|
mul_lt_one
theorem mul_lt_one :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b : α}, a < 1 → b < 1 → a * b < 1
This theorem, named `mul_lt_one`, states that for any type `α` that has multiplication and one as an identity (`MulOneClass α`), and has a preorder relation (`Preorder α`), if there exists a left covariance between multiplication and the less than relation (`CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1`), then for any two elements `a` and `b` of type `α`, if both `a` and `b` are less than one (`a < 1 → b < 1`), their multiplication will also be less than one (`a * b < 1`). The corresponding lemma assuming right covariance is denoted as `Right.mul_lt_one`.
More concisely: If `α` is a type with multiplication and one as an identity, a preorder relation, and covariance between multiplication and the less than relation, then `a * b < 1` for all `a, b ∈ α` such that `a, b < 1`.
|
Right.add_pos'
theorem Right.add_pos' :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α},
0 < a → 0 < b → 0 < a + b
The theorem `Right.add_pos'` states that for any type `α` that has an addition operation (satisfying `AddZeroClass` properties), an ordering (satisfying `Preorder` properties), and right-covariant addition (satisfying `CovariantClass` properties for the addition operation with arguments swapped), if `a` and `b` are elements of `α` and both are greater than zero, then their sum is also greater than zero. In mathematical notation, if `0 < a` and `0 < b`, then `0 < a + b`. This theorem assumes right covariance; the corresponding theorem for left covariance is `Left.add_pos'`.
More concisely: If `α` is a type with an `AddZeroClass`, `Preorder`, and `CovariantClass` for addition with arguments swapped, and `0 < a` and `0 < b` are elements of `α`, then `0 < a + b`.
|
Antitone.add_strictAnti
theorem Antitone.add_strictAnti :
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {f g : β → α},
Antitone f → StrictAnti g → StrictAnti fun x => f x + g x
This theorem states that for any types `α` and `β`, where `α` is a type with addition operation and `β` is a type following a preorder, given two functions `f` and `g` from `β` to `α`, if `f` is an antitone function (meaning that if `a ≤ b` then `f b ≤ f a`) and `g` is a strictly antitone function (meaning that if `a < b` then `f b < f a`), then the sum of these two functions, denoted as `f x + g x`, is also a strictly antitone function.
This theorem also requires two instances of `CovariantClass` for `α`, which ensure that addition behaves as expected with respect to the preorder relation: the first instance ensures that if `x < x_1` then `x + something < x_1 + something`, and the second instance ensures that if `x ≤ x_1` then `something + x ≤ something + x_1`.
More concisely: Given types `α` with an antisymmetric preorder and addition, and functions `f: β -> α` and `g: β -> α` where `f` is antitone and `g` is strictly antitone, then the function `x => f x + g x` is strictly antitone.
|
StrictMono.add_monotone
theorem StrictMono.add_monotone :
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α}
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1],
StrictMono f → Monotone g → StrictMono fun x => f x + g x
The theorem `StrictMono.add_monotone` states that, given any two functions `f` and `g` from a type `β` to a type `α`, where `α` is a type with addition and preorder relations, if `f` is strictly monotone (meaning that for any two elements where the first is less than the second, the function value of the first is also less than the function value of the second), and `g` is monotone (meaning that for any two elements where the first is less than or equal to the second, the function value of the first is also less than or equal to the function value of the second), then the function which maps each element to the sum of its `f` and `g` values is also strictly monotone. This also requires that `α` is a covariant class under addition and both less than or equal to and less than relations.
More concisely: If `f: β → α` is strictly monotone and `g: β → α` is monotone, then the function `h: β → α` defined by `h(x) := f(x) + g(x)` is strictly monotone, given that `α` is a covariant class under addition and preorder relations.
|
Contravariant.AddLECancellable
theorem Contravariant.AddLECancellable :
∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α]
[inst_2 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, AddLECancellable a
The theorem `Contravariant.AddLECancellable` states that for any type `α` equipped with addition and an order relation, if the type is a contravariant class, i.e., for all `x`, `y`, `z` in `α`, if `x + z ≤ y + z` implies `x ≤ y`, then every element `a` of the type `α` is 'AddLECancellable'. By 'AddLECancellable', it means that for any two elements `b` and `c` from the type `α`, if `a + b ≤ a + c` then `b ≤ c`. This is essentially saying that adding `a` to both sides of an inequality won't change the ordering of `b` and `c`.
More concisely: If `α` is a type equipped with addition and an order relation such that `α` is contravariant, then every element `a` in `α` satisfies `x ≤ y` whenever `a + x ≤ a + y`.
|
mul_le_mul'
theorem mul_le_mul' :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b c d : α},
a ≤ b → c ≤ d → a * c ≤ b * d
The theorem `mul_le_mul'` states that for any type `α` that has a `Mul` (multiplication) operation and is a `Preorder` (a type of order relation), if the multiplication operation is covariant in both arguments ("CovariantClass") and for any four elements `a`, `b`, `c`, and `d` of this type `α`, if `a` is less than or equal to `b` and `c` is less than or equal to `d`, then the product of `a` and `c` is less than or equal to the product of `b` and `d`. In mathematical terms, this is the standard property of ordered fields stating that the product of two numbers preserves the order when multiplying two inequalities.
More concisely: If `α` is a Preorder type with covariant Multiplication operation, then for all `a ≤ b` and `c ≤ d` in `α`, `a * c ≤ b * d`.
|
AntitoneOn.mul'
theorem AntitoneOn.mul' :
∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
[inst_3 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1],
AntitoneOn f s → AntitoneOn g s → AntitoneOn (fun x => f x * g x) s
This theorem is asserting that the product of two antitone functions is also antitone. Here, an antitone function is defined as a function `f` that is decreasing on a set `s`: if `a` and `b` are elements of `s` and `a` is less than or equal to `b`, then `f(b)` is less than or equal to `f(a)`. More specifically, given two functions `f` and `g` from some type `β` to `α`, both of which are antitone on a set `s`, and under the conditions that the type `α` supports multiplication operation and is a Preorder, and it is covariant under multiplication and its swapping operation, then the function defined by the product of `f(x)` and `g(x)` for each `x` in `β` is also antitone on the set `s`. This result can be useful in order theory and analysis.
More concisely: If `f` and `g` are antitone functions from a type `β` to a Preorder `α` with multiplication and covariant swapping, then their product `h(x) = f(x) * g(x)` is also an antitone function on the common domain of `f` and `g`.
|
Left.mul_lt_one'
theorem Left.mul_lt_one' :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α}, a < 1 → b < 1 → a * b < 1
This theorem, `Left.mul_lt_one'`, states that for any type `α` that has a multiplication operation and a one element (`MulOneClass α`), and that is also preordered (`Preorder α`), and with a left covariance property (`CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1`), if two elements `a` and `b` of this type are both less than one, then their product `a * b` is also less than one. A similar lemma that assumes right covariance is `Right.mul_lt_one'`.
More concisely: If `α` is a preordered type with one and multiplication, and `a, b ∈ α` satisfy `a, b < 1`, then `a * b < 1`.
|
Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.25
theorem Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.25 :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_3 : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α},
(a < b + a) = (0 < b)
This theorem, named `Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.25`, states that for any type `α` that is an additive zero class, has a less than operation, and satisfies both the covariant and contravariant properties with respect to the swap function involving addition and less than operation, for any element `a` of type `α` and any other element `b` of type `α`, the inequality `a` is less than `b + a` holds if and only if `0` is less than `b`.
More concisely: For any additive zero class type `α` with a total order satisfying the covariant and contravariant properties, `a` is less than `b + a` if and only if `0` is less than `b`.
|
StrictMono.add_const
theorem StrictMono.add_const :
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α}
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1],
StrictMono f → ∀ (c : α), StrictMono fun x => f x + c
The theorem `StrictMono.add_const` states that for any type `α` with an addition operation and a preorder relation, and any type `β` with a preorder relation, if `f` is a strictly monotone function from `β` to `α`, and `α` has a covariant class with respect to addition and the `<` relation, then adding a constant `c` to `f(x)` results in a function that is also strictly monotone. In simpler terms, adding a constant to a strictly increasing function does not change its strictly increasing property.
More concisely: If `f` is a strictly monotone function from a preordered type `β` to a type `α` with covariant addition and preorder relation, then the function `x ↦ f(x) + c` is also strictly monotone for any constant `c` in `α`.
|
add_lt_add
theorem add_lt_add :
∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c d : α},
a < b → c < d → a + c < b + d
This theorem, named `add_lt_add`, states that for a type `α` that has an addition operation and is a preorder (i.e., it has a binary relation that is reflexive and transitive), given the covariant classes for the addition operation, if `a` and `b` are elements of this type such that `a` is less than `b`, and `c` and `d` are also elements of this type such that `c` is less than `d`, then the sum of `a` and `c` is less than the sum of `b` and `d`. This theorem is an alias of `add_lt_add_of_lt_of_lt`. The function `Function.swap` is used to indicate that the binary operation and the less-than relation can be swapped in their arguments without changing their meaning.
More concisely: If `α` is a preorder type with a reflexive and transitive relation `≤`, and `a ≤ b` and `c ≤ d` in `α`, then `a + c ≤ b + d`.
|
Right.one_lt_mul_of_lt_of_le
theorem Right.one_lt_mul_of_lt_of_le :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b : α},
1 < a → 1 ≤ b → 1 < a * b
The theorem `Right.one_lt_mul_of_lt_of_le` states that for any type `α` endowed with a multiplication operation forming a unitary structure (`MulOneClass α`) and a preorder relationship (`Preorder α`), if the type `α` also possesses a right covariance property (`CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1`), then for any two elements `a` and `b` of `α`, if `1` is less than `a` and `1` is less than or equal to `b`, then `1` is less than the product of `a` and `b` (`1 < a * b`). In other words, for a structure with multiplication and preorder that exhibits right covariance, if `a` is greater than `1` and `b` is at least `1`, then the product `a * b` is also greater than `1`.
More concisely: Given a type `α` with a multiplication operation forming a unitary structure, a preorder relation, and right covariance, if `1` is less than both `a` and `b` in `α`, then `1` is less than their product `a * b`.
|
add_le_add
theorem add_le_add :
∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c d : α},
a ≤ b → c ≤ d → a + c ≤ b + d
This theorem, named `add_le_add`, states that for any type `α` that has an addition operation (`Add α`), a preorder relation (which is a reflexive and transitive binary relation), and satisfies the covariance properties for addition and order, if `a` and `b` are elements of `α` such that `a` is less than or equal to `b`, and `c` and `d` are elements of `α` such that `c` is less than or equal to `d`, then `a + c` is less than or equal to `b + d`. In conventional mathematical notation, this can be written as: ∀a, b, c, d ∈ `α`, if a ≤ b and c ≤ d, then a + c ≤ b + d. This theorem essentially formalizes one of the key properties of ordered rings.
More concisely: For any type `α` with an addition operation and a preorder relation that is covariant with respect to addition, if `a ≤ b` and `c ≤ d` in `α`, then `a + c ≤ b + d`.
|
one_lt_mul'
theorem one_lt_mul' :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b : α}, 1 < a → 1 < b → 1 < a * b
This theorem, named `one_lt_mul'`, states that for any type `α` equipped with a multiplication operation and a preorder, if the multiplication operation is left covariant (meaning that multiplying by a larger factor on the left results in a larger product), then if `a` and `b` are elements of `α` such that both `a` and `b` are greater than 1, their multiplication `a * b` is also greater than 1. The corresponding theorem for right covariance is `Right.one_lt_mul`.
More concisely: If `α` is a type with a left covariant multiplication operation and preorder, then for all `a, b ∈ α` with `a, b > 1`, we have `a * b > 1`.
|
le_mul_of_one_le_left'
theorem le_mul_of_one_le_left' :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α},
1 ≤ b → a ≤ b * a
This theorem states that for any type `α` that is equipped with multiplication operation, identity element for multiplication (`1`), and a less than or equal to order relation (`≤`), and also satisfies the property of covariance with respect to multiplication and the order relation, if a given element `b` of this type is greater than or equal to `1`, then any other element `a` of this type is less than or equal to the product of `b` and `a` (i.e., `b * a`). In mathematical notation, if `α` is a monoid under multiplication with a partial order `≤` that is covariant and `1 ≤ b`, then we have `a ≤ b * a` for all `a` in `α`.
More concisely: In a monoid `α` with a covariant partial order `≤` and identity element `1`, if `1 ≤ b` then `a ≤ b * a` for all `a` in `α`.
|
add_lt_of_le_of_neg
theorem add_lt_of_le_of_neg :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α},
b ≤ c → a < 0 → b + a < c
This theorem, `add_lt_of_le_of_neg`, states that given a type `α` which has an addition operation and a zero element (`AddZeroClass α`), also has a preorder relationship (`Preorder α`), and is a Covariant class where addition of two elements `x` and `x_1` results in a relationship `x < x_1`, then for any three elements `a`, `b`, and `c` of type `α`, if `b` is less than or equal to `c` (`b ≤ c`) and `a` is less than zero (`a < 0`), it follows that `b + a` is less than `c` (`b + a < c`). This captures an essential property of ordered additive structures.
More concisely: If `α` is an additive preordered type with `a < 0` and `b ≤ c`, then `b + a < c`.
|
lt_add_of_le_of_pos
theorem lt_add_of_le_of_pos :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α},
b ≤ c → 0 < a → b < c + a
The theorem `lt_add_of_le_of_pos` states that for any type `α` that has an addition operation and a zero element (`AddZeroClass`), a preorder relation (`Preorder`), and obeys the property that adding an element to both sides of a relation preserves the order (`CovariantClass`), if `b` is less than or equal to `c` and `a` is greater than zero, then `b` is less than the sum of `c` and `a`. This theorem essentially formalizes the idea that adding a positive number to a value makes the result greater, under certain conditions.
More concisely: If `α` is an additive preorder type with zero `0` and `a > 0`, then for all `b ≤ c`, we have `b < c + a`.
|
Left.one_le_mul
theorem Left.one_le_mul :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α}, 1 ≤ a → 1 ≤ b → 1 ≤ a * b
This theorem, `Left.one_le_mul`, states that given a type `α` equipped with a multiplication operation and a preorder, and assuming left covariance, for any two elements `a` and `b` of this type, if both `a` and `b` are greater than or equal to one, then their product `a * b` is also greater than or equal to one. A similar lemma exists for right covariance, named `Right.one_le_mul`.
More concisely: Given a preordered type with left covariant multiplication, if both `a` and `b` are greater than or equal to one, then `a * b` is also greater than or equal to one.
|
Left.add_pos_of_pos_of_nonneg
theorem Left.add_pos_of_pos_of_nonneg :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, 0 < a → 0 ≤ b → 0 < a + b
This theorem, `Left.add_pos_of_pos_of_nonneg`, assumes left covariance. Given a type `α` that has an addition operation, an order operation, and satisfies the covariance property, the theorem states that for any elements `a` and `b` of this type, if `a` is positive (i.e., `0 < a`) and `b` is nonnegative (i.e., `0 ≤ b`), then the sum of `a` and `b` is also positive (i.e., `0 < a + b`). Note that this theorem assumes left covariance, and a corresponding lemma for the case of right covariance is `Right.add_pos_of_pos_of_nonneg`.
More concisely: If `α` is an additive type with a total order such that `0 < a` and `0 ≤ b`, then `0 < a + b`. (Assumes left covariance.)
|
add_le_add_right
theorem add_le_add_right :
∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α]
[i : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {b c : α},
b ≤ c → ∀ (a : α), b + a ≤ c + a
The theorem `add_le_add_right` in Lean 4 states that for any type `α` that has an addition operation (`Add α`) and a less or equal to relation (`LE α`), and for this type if it holds that swapping the order of two arguments of the addition operation does not change the order of the relation (which is the property described by the `CovariantClass`), then for any two elements `b` and `c` of this type such that `b` is less than or equal to `c`, and for any other element `a` of this type, the inequality `b + a ≤ c + a` is always true. In other words, adding the same value to both sides of an inequality does not affect the inequality.
More concisely: For types `α` with covariant addition `(Add α)` and order relation `(LE α)`, if swapping addends preserves the order, then for all `a`, `b`, and `c` in `α` with `b ≤ c`, we have `b + a ≤ c + a`.
|
le_mul_of_le_of_one_le
theorem le_mul_of_le_of_one_le :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b c : α},
b ≤ c → 1 ≤ a → b ≤ c * a
The theorem `le_mul_of_le_of_one_le` states that for any type `α` that supports multiplication and the operation of "one" (`MulOneClass`), along with a preorder relationship (`Preorder`), and a specific covariance relationship (`CovariantClass`), if `b` is less than or equal to `c` and `1` is less than or equal to `a`, then `b` is less than or equal to `c` multiplied by `a`. This theorem is essentially asserting a property related to the ability to scale inequalities by multiplication in certain structures.
More concisely: If `a` is non-negative and `b` is less than or equal to `c`, then `b` is less than or equal to `c` multiplied by `a`.
|
add_pos
theorem add_pos :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α}, 0 < a → 0 < b → 0 < a + b
The `add_pos` theorem states that for any type `α` that is an instance of `AddZeroClass` and `Preorder` and where addition (`+`) is a `CovariantClass`, if `a` and `b` are such that both `a` and `b` are greater than zero (`0`), then the sum of `a` and `b` is also greater than zero. Specifically, if `0 < a` and `0 < b`, then `0 < a + b`. This is an alias of the `Left.add_pos` theorem.
More concisely: If `α` is a type with `AddZeroClass`, `Preorder`, and covariant addition, and `0 < a` and `0 < b` hold in `α`, then `0 < a + b`.
|
lt_of_add_lt_add_right
theorem lt_of_add_lt_add_right :
∀ {α : Type u_1} [inst : Add α] [inst_1 : LT α]
[i : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α},
b + a < c + a → b < c
This theorem, `lt_of_add_lt_add_right`, states that for any type `α` that has addition (`Add`), less than operation (`LT`), and for which the addition operation (`x + x_1`) is contravariant (i.e., if `x + a` decreases when `x` increases, given the condition `x < x_1`), then if `b + a` is less than `c + a`, it follows that `b` is less than `c`. In other words, if adding the same value `a` to two quantities `b` and `c` results in a smaller sum for `b + a` compared to `c + a`, then `b` is less than `c`. This is a property related to the cancellation law in ordered additive groups.
More concisely: If `α` is an additive type with contravariant addition and `x < x_1`, then `b LT c` implies `b + a LT c + a`.
|
StrictAnti.mul'
theorem StrictAnti.mul' :
∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α}
[inst_3 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1],
StrictAnti f → StrictAnti g → StrictAnti fun x => f x * g x
The theorem `StrictAnti.mul'` states that if we have two functions `f` and `g` that are strictly antitone (meaning for any two elements, say `a` and `b`, in the set `β` with `a < b`, we have `f b < f a` and `g b < g a`), then their product is also a strictly antitone function. This is under the conditions that multiplication and the less-than operation on the set `α` satisfy certain covariance properties.
More concisely: If `f` and `g` are strictly antitone functions, then their product is also a strictly antitone function, under the assumption that multiplication and the less-than relation on `α` are covariant.
|
one_lt_mul_of_lt_of_le'
theorem one_lt_mul_of_lt_of_le' :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α}, 1 < a → 1 ≤ b → 1 < a * b
This theorem, named `one_lt_mul_of_lt_of_le'`, states that for a type `α` with multiplication and order properties (specifically, `α` is a multiplication-one class and preorder), along with the property of left covariance, if we have two elements `a` and `b` of `α` such that `a` is greater than one and `b` is greater than or equal to one, then the product `a * b` is also greater than one. The equivalent lemma assuming right covariance is `Right.one_lt_mul_of_lt_of_le`.
More concisely: If `α` is a preorder type with multiplication and `a, b ∈ α` such that `1 < a` and `1 ≤ b`, then `a * b > 1`.
|
add_neg
theorem add_neg :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α}, a < 0 → b < 0 → a + b < 0
The theorem `add_neg` is an alias of `Left.add_neg`. It states that for any type `α` that is an instance of `AddZeroClass` and `Preorder`, and is a `CovariantClass` for addition and a strict less-than comparison, if `a` and `b` are of type `α` and both less than zero, then their sum `a + b` is also less than zero. In other words, the sum of two negative values in this context is also a negative value.
More concisely: If `α` is a type with additive and preorder structures, and `a` and `b` are negative elements of `α`, then `a + b` is also a negative element.
|
Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.6
theorem Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.6 :
∀ {α : Type u_1} [inst : Add α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b c : α},
(a + b < a + c) = (b < c)
This theorem states that for any type `α` which is equipped with an addition operation and a less-than relation, along with two other conditions (known as CovariantClass and ContravariantClass) related to the interaction of addition and the less-than relation, the inequality between `a + b` and `a + c` is equivalent to the inequality between `b` and `c`. In other words, if `a`, `b`, and `c` are elements of type `α`, then `a + b` is less than `a + c` if and only if `b` is less than `c`. This theorem encapsulates the principle of monotonicity of addition in ordered additive monoids.
More concisely: For any additive monoid with a total order, the addition operation is monotonic with respect to the order relation. That is, for all `a, b, c` in the monoid, `a + b` is less than `a + c` if and only if `b` is less than `c`.
|
Left.mul_lt_mul
theorem Left.mul_lt_mul :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b c d : α},
a < b → c < d → a * c < b * d
This theorem, `Left.mul_lt_mul`, states that for any type `α` equipped with a multiplication operation and a preorder (a reflexive and transitive binary relation), and assuming that the type is left strictly covariant and also left covariant in a non-strict manner under multiplication, if `a` and `b` are elements of type `α` such that `a` is less than `b`, and `c` and `d` are also elements of type `α` with `c` less than `d`, then the product `a * c` is less than the product `b * d`. This is essentially a statement about the preservation of order under multiplication in this mathematical structure.
More concisely: If `α` is a type with a multiplication operation and a preorder, and `α` is left strictly covariant and covariant under multiplication, then `a < b` and `c < d` imply `a * c < b * d`.
|
Left.add_neg'
theorem Left.add_neg' :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, a < 0 → b < 0 → a + b < 0
This theorem, `Left.add_neg'`, states that for any type `α` that has an addition operation (satisfying the properties of associativity and having a zero element), a preorder (a binary relation that is reflexive and transitive), and exhibits left covariance (meaning addition of elements respects the preorder), if two elements `a` and `b` are both less than zero, then their sum `a + b` is also less than zero. The lemma assuming right covariance is `Right.add_neg'`.
More concisely: If `α` is a type with an associative addition operation, a zero element, and exhibits left covariance in a preorder, then for all `a, b ∈ α`, if `a ≤ b` and `b < 0`, then `a + b < 0`.
|
add_neg_of_nonpos_of_neg
theorem add_neg_of_nonpos_of_neg :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α}, a ≤ 0 → b < 0 → a + b < 0
This theorem, `add_neg_of_nonpos_of_neg`, is essentially an alias of `Left.add_neg_of_nonpos_of_neg`. It states that for any type `α`, which is an additive zero class and has a preorder (a binary relation that is reflexive and transitive), and also satisfies the covariance property (in this case for addition and less than relation), if you have two elements `a` and `b` from `α` such that `a` is less than or equal to zero and `b` is less than zero, then their sum `a + b` is also less than zero.
More concisely: For any additive zero class α with a preorder and covariance property, if a and b are elements of α with a ≤ 0 and b < 0, then a + b < 0.
|
add_lt_add_left
theorem add_lt_add_left :
∀ {α : Type u_1} [inst : Add α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {b c : α},
b < c → ∀ (a : α), a + b < a + c
This theorem, `add_lt_add_left`, states that for any type `α` with an addition operation and a less-than relation, if the type has the covariant property for addition and less-than (where adding a value to two items maintains their original order), then for any two elements `b` and `c` of this type, if `b` is less than `c`, adding another element `a` to both `b` and `c` results in `a + b` still being less than `a + c`. This theorem essentially formalizes the intuitive property that adding the same value to two different numbers maintains their relative ordering.
More concisely: If `α` is a type with covariant addition and less-than relations, then for all `a`, `b`, and `c` in `α` with `b < c`, we have `a + b < a + c`.
|
StrictMono.mul_monotone'
theorem StrictMono.mul_monotone' :
∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α}
[inst_3 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1],
StrictMono f → Monotone g → StrictMono fun x => f x * g x
The theorem states that given a multiplication and preorder structure on types `α` and `β`, and let `f` and `g` be functions from `β` to `α`. Also, given that multiplication on `α` is both left and right covariant. If `f` is a strictly monotone function and `g` is a monotone function, then the function that maps `x` to the product of `f(x)` and `g(x)` - `f x * g x`, is strictly monotone. In other words, if `a < b` implies `f(a) < f(b)` (strictly monotone) and `a ≤ b` implies `g(a) ≤ g(b)` (monotone), then `a < b` implies `f(a)*g(a) < f(b)*g(b)`.
More concisely: Given multiplication and preorder structures on types `α` and `β`, if `f: β → α` is strictly monotone and `g: β → α` is monotone, then the function `x => f x * g x` is strictly monotone on `β`.
|
Left.mul_le_one
theorem Left.mul_le_one :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α}, a ≤ 1 → b ≤ 1 → a * b ≤ 1
This theorem, `Left.mul_le_one`, states that for any type `α` equipped with a multiplication operation, a one element, and a preorder relation that is left-covariant with respect to multiplication, if `a` and `b` are elements of `α` such that both `a` and `b` are less than or equal to `1`, then the product `a * b` is also less than or equal to `1`. In other words, in a structure with these properties, the product of two elements that are each no greater than one is also no greater than one. Note that this theorem assumes left covariance; an analogous theorem for right covariance is `Right.mul_le_one`.
More concisely: In a preorder equipped with a multiplication and a one element, if both multiplicands are less than or equal to one, then their product is less than or equal to one (assuming left-covariance with respect to multiplication).
|
mul_lt_one_of_lt_of_le
theorem mul_lt_one_of_lt_of_le :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α}, a < 1 → b ≤ 1 → a * b < 1
This theorem, `mul_lt_one_of_lt_of_le`, states that for any type `α` that is a multiplication unit class and has a preorder relation, and is left covariant, if we have two elements `a` and `b` of type `α`, then if `a` is less than `1` and `b` is less than or equal to `1`, the product of `a` and `b` is less than `1`. This is an alias of the theorem `Left.mul_lt_one_of_lt_of_le`, and the equivalent lemma for right covariance is `Right.mul_lt_one_of_lt_of_le`.
More concisely: For any multiplication unit class `α` with a preorder relation that is left covariant, if `a` and `b` are elements of `α` with `0 < a` and `0 <= b`, then `a * b < 1`.
|
add_le_of_nonpos_left
theorem add_le_of_nonpos_left :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α},
b ≤ 0 → b + a ≤ a
This theorem, `add_le_of_nonpos_left`, is a statement about an ordered additive structure. Specifically, for any type `α` that has an additive zero, an addition operation, a less-than-or-equal-to relation, and satisfies the covariance property for addition and this relation (i.e., for all `x` and `y` in `α`, `x + y ≤ x` implies `y ≤ 0`), if `b` is a non-positive element of `α` (i.e., `b ≤ 0`), then adding `b` to any element `a` of `α` will result in a sum that is less than or equal to `a`.
More concisely: For any additive structure `α` with covariance for addition and a non-positive element `b`, `a + b ≤ a` for all `a` in `α`.
|
Right.mul_lt_one'
theorem Right.mul_lt_one' :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α},
a < 1 → b < 1 → a * b < 1
This theorem, titled `Right.mul_lt_one'`, states that for any type `α` that has multiplication and a one element (`MulOneClass α`), an order relation (`Preorder α`), and satisfies right covariance (`CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1`), if two elements `a` and `b` of this type are both less than one, then their product `a * b` is also less than one. The right covariance condition here ensures that multiplication distributes over the order: if `x ≤ y`, then `b * x ≤ b * y` for any `b`. This is the counterpart to a similar theorem `Left.mul_lt_one'` which assumes left covariance, where the inequality holds with multiplication on the other side: if `x ≤ y`, then `x * b ≤ y * b` for any `b`.
More concisely: Given a type `α` with multiplication, a one element, an order relation, and right covariance, if `a` and `b` are both less than one, then their product `a * b` is also less than one.
|
add_pos_of_nonneg_of_pos
theorem add_pos_of_nonneg_of_pos :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α}, 0 ≤ a → 0 < b → 0 < a + b
The theorem `add_pos_of_nonneg_of_pos` is essentially an alias of `Left.add_pos_of_nonneg_of_pos`. It states that for any type `α` that has an addition operation (where `0` is the identity element) and a preorder relation (i.e., a binary relation that is reflexive and transitive), and also has a covariant class (essentially meaning that addition preserves the order), if `a` and `b` are elements of `α` such that `a` is non-negative (0 ≤ a) and `b` is positive (0 < b), then the sum of `a` and `b` is also positive (0 < a + b).
More concisely: If `α` is a type with an addition operation, identity element `0`, a preorder relation that is reflexive, transitive, and covariant, and `0 ≤ a` and `0 < b` hold for elements `a, b ∈ α`, then `0 < a + b`.
|
Left.one_lt_mul_of_lt_of_le
theorem Left.one_lt_mul_of_lt_of_le :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α}, 1 < a → 1 ≤ b → 1 < a * b
This theorem states that for any type `α` that has multiplication and order defined on it (specifically, a multiplication with a "one" element and an order that is a preorder), and if multiplication on `α` is "left covariant", then for any elements `a` and `b` of `α`, if `1` is less than `a` and `1` is less than or equal to `b`, then `1` is less than the product `a * b`. Here, "left covariant" means that for any elements `x`, `y`, and `z` of `α`, if `x` is less than or equal to `y`, then `z * x` is less than or equal to `z * y`.
More concisely: If `α` is a type with a preorder and left covariant multiplication, then for all `a`, `b` in `α` with `1` less than both `a` and `b`, it follows that `1` is less than `a * b`.
|
add_neg_of_neg_of_nonpos
theorem add_neg_of_neg_of_nonpos :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, a < 0 → b ≤ 0 → a + b < 0
This theorem, `add_neg_of_neg_of_nonpos`, is an alias of `Left.add_neg_of_neg_of_nonpos`. It states that for any type `α` that is an additive group with a zero element, and that has a preorder and a covariance property defined on it, if we have two elements `a` and `b` from this type such that `a` is less than zero and `b` is less than or equal to zero, then their sum `a + b` will be less than zero.
More concisely: If `α` is an additive group with a zero element and a preorder such that `a < 0` and `b <= 0` imply `a + b < 0`, then this property holds.
|
one_lt_mul''
theorem one_lt_mul'' :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α}, 1 < a → 1 < b → 1 < a * b
This theorem states that, given a type `α` equipped with a multiplication operation and a preorder relation, and assuming left covariance for multiplication and the preorder relation, if two elements `a` and `b` of the type are both greater than 1, then their product is also greater than 1. The alias for this theorem with right covariance is `Right.one_lt_mul'`.
More concisely: Given a preorder `(α, ≤)` and a multiplication `(*: α → α → α)` on type `α` such that multiplication is left covariant with respect to the preorder, if `a` and `b` are elements of `α` with `a ≤ b` and `a > 1` and `b > 1`, then `a * b > 1`.
|
le_add_of_le_of_nonneg
theorem le_add_of_le_of_nonneg :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α},
b ≤ c → 0 ≤ a → b ≤ c + a
This theorem, `le_add_of_le_of_nonneg`, states that for any type `α` that has an addition operation, a zero element, and a preorder relation (basically, a mathematical structure where you can add elements, have a concept of zero, and compare elements), and if addition of elements respects the preorder relation, then for any three elements `a`, `b`, and `c` of type `α`, if `b` is less than or equal to `c`, and `a` is non-negative (greater than or equal to zero), then `b` is less than or equal to the sum of `c` and `a`. This is a generalization of a common property in number systems: if `b` ≤ `c` and `a` ≥ 0, then `b` ≤ `c` + `a`.
More concisely: If `α` is a type with addition, zero, and a preorder relation such that `a ≤ b` implies `a + c ≤ b + c` for all `a, b, c` in `α` with `a` non-negative, then `b ≤ c` implies `b ≤ c + a`.
|
lt_mul_of_one_le_of_lt
theorem lt_mul_of_one_le_of_lt :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b c : α},
1 ≤ a → b < c → b < a * c
The theorem `lt_mul_of_one_le_of_lt` states that for any type `α` that has a multiplication and one operation (`MulOneClass α`), and is a preorder (Preorder α) and a covariant class, and for any elements `a`, `b`, `c` of type `α`, if `1` is less than or equal to `a` and `b` is less than `c`, then `b` is less than the product of `a` and `c`. This theorem essentially states that if `a` is at least `1` and `b` is smaller than `c`, then `b` is also smaller than the result of multiplying `a` and `c`, under the conditions of the type `α`.
More concisely: If `α` is a preorder type with multiplication and one operation, and `1 ≤ a` and `b < c`, then `b < a * c`.
|
Monotone.mul_strictMono'
theorem Monotone.mul_strictMono' :
∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {f g : β → α},
Monotone f → StrictMono g → StrictMono fun x => f x * g x
The theorem `Monotone.mul_strictMono'` states that for any types `α` and `β`, with `α` having an operation of multiplication and being a preorder (a set where you can tell whether one element is less than, equal to, or greater than another), and `β` also being a preorder, if we have the covariant properties that multiplying two elements in `α` preserves their order (`x < x_1` implies `x * x_1 < x * x_1`) and that swapping the multiplication order also preserves non-strict order (`x ≤ x_1` implies `x_1 * x ≤ x_1 * x`), then given a monotone function `f` and a strictly monotone function `g` from `β` to `α`, the function that maps `x` to the product of `f(x)` and `g(x)` is strictly monotone.
In other words, the product of a function that preserves order and a function that strictly preserves order also strictly preserves order. This is under the condition that the multiplication operation in the codomain type respects the order of elements and that swapping the order of multiplication still preserves the order.
More concisely: If `α` is a preordered type with covariantly multiplicative order, `β` is another preordered type, `f : β → α` is monotone, `g : β → α` is strictly monotone, and multiplication in `α` is order-preserving and commutative, then the composition of `f` and `g` is a strictly monotone function.
|
add_lt_add_right
theorem add_lt_add_right :
∀ {α : Type u_1} [inst : Add α] [inst_1 : LT α]
[i : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {b c : α},
b < c → ∀ (a : α), b + a < c + a
The theorem `add_lt_add_right` states that for any type `α` that supports addition and a `<` operation (strictly less than), and satisfies the `CovariantClass` property (which essentially means that if `x` is less than `y`, then `x + z` is less than `y + z` for all `z`), if `b` is less than `c`, then for all `a`, the result of adding `a` to `b` is less than the result of adding `a` to `c`. In other words, for all real numbers `a`, `b` and `c`, if `b < c`, then `b + a < c + a`.
More concisely: For types `α` with addition and a covariant `<` relation, if `b < c`, then for all `a`, `b + a < c + a`.
|
le_of_mul_le_mul_right'
theorem le_of_mul_le_mul_right' :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : LE α]
[i : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b c : α},
b * a ≤ c * a → b ≤ c
This theorem, named `le_of_mul_le_mul_right'`, asserts that for any type `α` that has a multiplication operation (`Mul α`), an order relation (`LE α`), and satisfies the contravariant property with respect to multiplication and this order (expressed by `ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1`), if the product of `b` and `a` is less than or equal to the product of `c` and `a`, then `b` is less than or equal to `c`. In other words, if multiplying `a` with `b` results in a value that is not larger than multiplying `a` with `c`, then `b` is not larger than `c`, given that multiplication and order relation follow the described contravariant property.
More concisely: If `α` is a type with multiplication and order relation satisfying the given contravariance property, and `a` is an element of `α`, then `b ≤ c` if and only if `a * b ≤ a * c`.
|
mul_lt_mul_iff_right
theorem mul_lt_mul_iff_right :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1]
[inst_3 : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] (a : α) {b c : α},
b * a < c * a ↔ b < c
The theorem `mul_lt_mul_iff_right` states that for any type `α` equipped with a multiplication operation and a less-than relation, and which satisfies the properties of being a covariant and a contravariant class under multiplication (i.e., multiplication preserves the order), if you have three elements `a`, `b`, and `c` of this type, then `b` times `a` is less than `c` times `a` if and only if `b` is less than `c`. This essentially states that multiplication by a fixed element on the right-hand side preserves the order of elements.
More concisely: For any type equipped with a multiplication and a total order such that multiplication is covariant and contravariant, the relation a \* b < a \* c holds if and only if b < c.
|
add_le_add_left
theorem add_le_add_left :
∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {b c : α},
b ≤ c → ∀ (a : α), a + b ≤ a + c
This theorem, `add_le_add_left`, states that for any type `α` with addition and a less than or equal to order that is covariant under addition, if `b` is less than or equal to `c`, then for any `a`, the sum of `a` and `b` is less than or equal to the sum of `a` and `c`. In simpler terms, if one number `b` is less than or equal to another number `c`, then adding the same number `a` to both `b` and `c` will preserve this inequality.
More concisely: For all types `α` with covariant addition and order `≤`, if `b ≤ c` then `a + b ≤ a + c`.
|
add_lt_add_of_lt_of_le
theorem add_lt_add_of_lt_of_le :
∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c d : α},
a < b → c ≤ d → a + c < b + d
The `add_lt_add_of_lt_of_le` theorem states that for any type `α` that is an instance of the `Add` and `Preorder` classes and respects the covariance property over addition and comparison functions, then for any four elements `a`, `b`, `c`, and `d` from `α`, if `a` is less than `b` and `c` is less than or equal to `d`, it implies that the sum of `a` and `c` is less than the sum of `b` and `d`. This is a principle of order theory which states that if you have two ordered pairs where the first element of the first pair is less than the first element of the second pair and the second element of the first pair is less than or equal to the second element of the second pair, then the sum of the elements of the first pair is less than the sum of the elements of the second pair.
More concisely: For elements `a`, `b`, `c`, `d` of a type `α` with the Add and Preorder instances satisfying covariance property: `a < b` and `c <= d` imply `a + c < b + d`.
|
Antitone.mul'
theorem Antitone.mul' :
∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α}
[inst_3 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1],
Antitone f → Antitone g → Antitone fun x => f x * g x
This theorem states that the product of two antitone functions is also an antitone function. Specifically, given a multiplication operation on a type `α` and a preorder relation on types `α` and `β`, if two functions `f` and `g` from `β` to `α` are antitone, and `α` satisfies covariant properties for both direct and swapped multiplication, then the function that maps `x` in `β` to the product of `f(x)` and `g(x)` in `α` is also antitone. An antitone function is one where if `a` is less than or equal to `b`, then `f(b)` is less than or equal to `f(a)`.
More concisely: If two antitone functions map a preordered type to a covariantly multiplicative type, then their product is an antitone function.
|
mul_le_mul_iff_right
theorem mul_le_mul_iff_right :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a : α) {b c : α},
b * a ≤ c * a ↔ b ≤ c
The theorem `mul_le_mul_iff_right` states that for any type `α` that supports multiplication (`Mul α`) and a less-than-or-equal-to relation (`LE α`), and satisfies both the `CovariantClass` and `ContravariantClass` conditions for multiplication and the less-than-or-equal-to relation, for every element `a` of type `α`, and for all `b` and `c` of type `α`, the inequality `b * a ≤ c * a` holds if and only if `b ≤ c`.
In mathematical terms, this says that for a given `a`, multiplication by `a` from the right preserves the order of `b` and `c`. That is, if `b` is less than or equal to `c`, then `b * a` is also less than or equal to `c * a`, and vice versa. This property is crucial for defining ordered rings and fields.
More concisely: For any type `α` with multiplication and a bilaterally ordered structure, the inequality `b ≤ c` is equivalent to `b * a ≤ c * a` for all `a, b, c ∈ α`.
|
le_add_iff_nonneg_left
theorem le_add_iff_nonneg_left :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α},
a ≤ b + a ↔ 0 ≤ b
This theorem, `le_add_iff_nonneg_left`, states that for any type `α` equipped with an addition operation and a less-than-or-equal-to (`≤`) relation satisfying specific properties (these properties are encoded by the `AddZeroClass`, `CovariantClass`, and `ContravariantClass` classes), for any elements `a` and `b` of `α`, the element `a` is less than or equal to `b` added to `a` if and only if `0` is less than or equal to `b`. In mathematical terms, this theorem states that for all `a` and `b` in `α`, `a ≤ b + a` is equivalent to `0 ≤ b`.
More concisely: For any type `α` with Addition and `≤` relation satisfying certain properties, `a ≤ b + a` if and only if `0 ≤ b`.
|
Right.add_pos
theorem Right.add_pos :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α},
0 < a → 0 < b → 0 < a + b
This theorem, named `Right.add_pos`, asserts that for any type `α` equipped with an addition and zero (`AddZeroClass`), a preorder (reflexive and transitive binary relation), and a right covariant class (which ensures that swapping the arguments of the addition operation preserves the order), if `a` and `b` are elements of `α` such that both `a` and `b` are greater than zero, then the sum of `a` and `b` is also greater than zero. This is under the assumption of right covariance; there exists a corresponding lemma for left covariance named `Left.add_pos`.
More concisely: For any type `α` with an `AddZeroClass` structure, a preorder, and right covariance, if `a` and `b` are positive elements, then `a + b` is also positive.
|
Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.2
theorem Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.2 :
∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) {b c : α},
(a + b ≤ a + c) = (b ≤ c)
This theorem, from the Mathlib library in Lean, states that for all types `α`, if `α` is a type that has addition and order defined, satisfies the CovariantClass property and the ContravariantClass property (both with respect to addition and order), then for any `a`,`b`, and `c` of type `α`, the inequality `a + b ≤ a + c` is equivalent to `b ≤ c`. In other words, adding an equal amount to both sides of an inequality doesn't change the inequality, an essential and intuitive property of ordered additive structures.
More concisely: If `α` is an additive and ordered type with Covariant and Contravariant classes of inequalities, then for all `a, b, c` in `α`, `a + b ≤ a + c` if and only if `b ≤ c`.
|
lt_add_iff_pos_right
theorem lt_add_iff_pos_right :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α},
a < a + b ↔ 0 < b
This theorem states that for any type `α` that forms an additive monoid and has a less-than (`<`) relation, and for any values `a` and `b` of type `α`, `a` is less than `a + b` if and only if `0` is less than `b`. The less-than relation is assumed to behave coherently with addition (meaning it respects the order of addition), as expressed by the `CovariantClass` and `ContravariantClass` instances.
More concisely: For any additive monoid type `α` with a covariant and contravariant order relation `<`, we have `a < a + b` if and only if `0 < b`.
|
lt_add_of_pos_left
theorem lt_add_of_pos_left :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α},
0 < b → a < b + a
The theorem `lt_add_of_pos_left` states that for any type `α` that has an addition operation, a zero element, and an order relation, and such that addition is covariant (namely, if `x < y` then `x + z < y + z`), if `b` is a positive element of type `α` (more precisely, `0 < b`), then `a` is less than `b + a`. In other words, if `b` is positive, then adding `b` to `a` results in a value that is greater than `a`.
More concisely: For any type `α` with addition, zero, and order relations where addition is covariant, if `0 < b` then `a < b + a`.
|
Left.add_nonpos
theorem Left.add_nonpos :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, a ≤ 0 → b ≤ 0 → a + b ≤ 0
This theorem, `Left.add_nonpos`, states that for any type `α` that has an addition operation (`AddZeroClass α`) and a preorder operation (`Preorder α`), and that satisfies the left covariance property (`CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1`), if `a` and `b` are elements of `α` such that both `a` and `b` are less than or equal to 0, then the sum of `a` and `b` is also less than or equal to 0. Essentially, it says that the sum of two non-positive elements in a left-covariant ordered additive class is also non-positive.
More concisely: In a left-covariant preordered additive type where the sum is less than or equal to the larger element, the sum of two non-positive elements is non-positive.
|
Right.mul_lt_mul
theorem Right.mul_lt_mul :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b c d : α},
a < b → c < d → a * c < b * d
The theorem `Right.mul_lt_mul` states that for any type `α` that has a multiplication operation (`Mul α`), an order relation (`Preorder α`), and satisfies the right strict covariance properties (`CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1` and `CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1`), if `a` and `b` are elements of `α` such that `a` is less than `b` and `c` and `d` are elements of `α` such that `c` is less than `d`, then the product of `a` and `c` is less than the product of `b` and `d`. This theorem assumes right strict covariance - that is, it assumes that the multiplication operation is strictly covariant when its arguments are swapped.
More concisely: If `α` is a type with a multiplication operation, an order relation, and right strict covariance properties, then for all `a < b` and `c < d` in `α`, we have `a * c < b * d`.
|
mul_le_mul_right'
theorem mul_le_mul_right' :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : LE α]
[i : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {b c : α},
b ≤ c → ∀ (a : α), b * a ≤ c * a
The theorem `mul_le_mul_right'` states that for any type `α` that supports multiplication and a "less than or equal to" comparison, and that maintains a certain covariant class property, if `b` and `c` are elements of `α` such that `b` is less than or equal to `c`, then for any other element `a` of `α`, the result of multiplying `b` by `a` is less than or equal to the result of multiplying `c` by `a`. In short, it proves the property of preserving the order under multiplication on the right in such a structure.
More concisely: For all types `α` with covariant multiplication and a total order, and for all `a`, `b`, and `c` in `α` with `b ≤ c`, we have `b * a ≤ c * a`.
|
Right.add_neg'
theorem Right.add_neg' :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α},
a < 0 → b < 0 → a + b < 0
The `Right.add_neg'` theorem states that for any type `α` which is an instance of the `AddZeroClass` (meaning it supports addition operation and has a zero element), and is a `Preorder` (meaning it has a relation `≤` that is reflexive and transitive), and satisfies the `CovariantClass` (meaning that if `x ≤ y`, then `f x ≤ f y` for the function `f` defined as the swap of the addition function), if `a` and `b` are elements of `α` such that both `a` and `b` are less than zero, then the sum of `a` and `b` is also less than zero. This theorem makes an assumption of right covariance, and there is a corresponding lemma for left covariance.
More concisely: If `α` is a type with AddZeroClass, Preorder structure where the addition is covariant, and `a`, `b` are elements of `α` both less than zero, then `a + b` is less than zero.
|
Right.mul_le_one
theorem Right.mul_le_one :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α},
a ≤ 1 → b ≤ 1 → a * b ≤ 1
This theorem, named "Right.mul_le_one", states that for any type `α` that is a `MulOneClass` (meaning it has multiplication and a multiplicative identity element) and a `Preorder` (meaning it has a binary relation that is reflexive and transitive), and for which the multiplication operation is right covariant (meaning that if `x ≤ y` then `x*z ≤ y*z` for all `z`), if we have two elements `a` and `b` of `α` such that `a` and `b` are both less than or equal to 1, then their product `a * b` is also less than or equal to 1.
More concisely: If `α` is a type with a multiplicative identity, is a Preorder with right covariant multiplication, and all elements have absolute value less than or equal to 1, then `a * b ≤ 1` for all `a, b ∈ α`.
|
mul_le_of_le_one_left'
theorem mul_le_of_le_one_left' :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α},
b ≤ 1 → b * a ≤ a
The theorem `mul_le_of_le_one_left'` states that for all types `α` that have a multiplication operation, a multiplicative identity (one), and a less than or equal to relation, and for which the multiplication operation is covariant with respect to the less than or equal to relation, if a given value `b` is less than or equal to 1, then the product of `b` and any other value `a` is less than or equal to `a`. In other words, if you multiply any number by a number that is less than or equal to one, the result will be less than or equal to the original number. This is written in mathematical notation as: for all `a` and `b` in `α`, if `b ≤ 1` then `b * a ≤ a`.
More concisely: For all types `α` with multiplication, identity one, and a covariant multiplication with respect to the <= relation, if `b <= 1` then `b * a <= a` for all `a` in `α`.
|
Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.17
theorem Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.17 :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α},
(a ≤ b + a) = (0 ≤ b)
The theorem, denoted as `Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.17`, states that for any type `α` that has an addition operation (`AddZeroClass α`), a less than or equal to operation (`LE α`), and satisfies both the covariant and contravariant properties for the swapping function (which switches the order of addition and comparison), the inequality `a ≤ b + a` is equivalent to `0 ≤ b`. The variables `a` and `b` are elements of type `α`. In more informal terms, this theorem is about a certain ordering property of additive monoids, stating that adding `a` to both sides of `0 ≤ b` does not change the truth value of the inequality.
More concisely: For any additive monoid type `α` with covariant and contravariant order properties, the inequality `a <= b` is equivalent to `0 <= b + a`.
|
mul_lt_mul_left'
theorem mul_lt_mul_left' :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {b c : α},
b < c → ∀ (a : α), a * b < a * c
This theorem, `mul_lt_mul_left'`, states that for any type `α` that has a multiplication operation, a less-than relation, and satisfies the covariant class property with respect to multiplication and the less-than relation, given two elements `b` and `c` of `α` where `b` is less than `c`, for any element `a` in `α`, the result of `a` multiplied by `b` is less than `a` multiplied by `c`. In other words, when multiplying by a common factor on the left, an inequality is preserved. This is a statement about the preservation of order under left multiplication in a certain class of ordered semigroups.
More concisely: For any covariant ordered semigroup `α` with respect to multiplication and the less-than relation, if `b` < `c` in `α`, then for all `a` in `α`, `a` * `b` < `a` * `c`.
|
Antitone.add
theorem Antitone.add :
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α}
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
Antitone f → Antitone g → Antitone fun x => f x + g x
The theorem `Antitone.add` states that for any two functions `f` and `g` from a preordered set `β` to an additive preordered set `α`, if both `f` and `g` are antitone (meaning that if `a ≤ b`, then `f b ≤ f a` and `g b ≤ g a`), then the function defined as the sum of `f` and `g` (for each x in `β`, it gives `f x + g x` in `α`) is also antitone. This is under the condition that `α` is a covariant class under the operation of addition, both in its standard order and when the arguments are swapped.
More concisely: If `α` is a covariant additive preorder with respect to addition, and `f` and `g` are antitone functions from a preordered set `β` to `α`, then the function `x => f x + g x` is antitone.
|
add_le_of_nonpos_right
theorem add_le_of_nonpos_right :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, b ≤ 0 → a + b ≤ a
This theorem states that for any type `α` that has addition and zero (`AddZeroClass`), a less than or equal to relation (`LE`), and obeys a certain covariance property (`CovariantClass` with respect to addition and the less than or equal to relation), if `b` is less than or equal to zero, then `a + b` is always less than or equal to `a`. In mathematical terms, it means for any `a` and `b` in `α`, if `b ≤ 0`, then `a + b ≤ a`. This aligns with the intuitive idea that adding a non-positive number to a given number doesn't increase the original number.
More concisely: For any type `α` with `AddZeroClass`, `LE`, and the covariance property `CovariantClass` for addition and `LE`, if `b ≤ 0`, then `a ≤ a + b`. (Note: This is the negation of the original statement to make it consistent with the usual mathematical convention that `a ≤ b` implies `a + c ≤ b + c` for all `c`.)
|
mul_le_mul_left'
theorem mul_le_mul_left' :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {b c : α},
b ≤ c → ∀ (a : α), a * b ≤ a * c
This theorem states that for any type `α` endowed with a multiplication operation and an order relation, under the condition that the type `α` obeys the "covariant" property (namely, if `x` and `x_1` are elements of `α` and `x ≤ x_1`, then `x * z ≤ x_1 * z` for any `z` in `α`), the multiplication operation is monotonic. More specifically, if `b` and `c` are elements of `α` and `b ≤ c`, then for any `a` in `α`, `a * b` is less than or equal to `a * c`.
More concisely: If `α` is a type with a covariant multiplication and order relation such that `x ≤ x_1` implies `x * z ≤ x_1 * z` for all `x, x_1, z` in `α`, then multiplication is monotonic, i.e., `b ≤ c` implies `a * b ≤ a * c` for all `a, b, c` in `α`.
|
lt_add_iff_pos_left
theorem lt_add_iff_pos_left :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_3 : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α},
a < b + a ↔ 0 < b
The theorem `lt_add_iff_pos_left` states that for any type `α` that has an addition operation, a zero element, and a less-than relation `LT` that satisfies both the covariant and contravariant properties, for any elements `a` and `b` of this type, the inequality `a < b + a` is true if and only if `0 < b`. This theorem establishes a connection between an inequality involving addition and a simple inequality with zero, which could be useful for simplifying expressions or proving other statements about the type `α`.
More concisely: For any type `α` with addition, zero, and a transitive and reflexive relation `LT`, we have `a < b + a` if and only if `0 < b`.
|
Left.add_lt_add
theorem Left.add_lt_add :
∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c d : α},
a < b → c < d → a + c < b + d
The theorem `Left.add_lt_add` states that for any ordered set `α` which is equipped with addition, and assuming that `α` has both strict left covariance and weak right covariance properties, if `a` is less than `b` and `c` is less than `d` (where `a`, `b`, `c`, and `d` are elements of `α`), then `a + c` is less than `b + d`. In other words, if we have two pairs of elements where in each pair the first element is less than the second one, the sum of the lesser elements will be less than the sum of the greater elements.
More concisely: If `α` is an ordered additive semigroup with strict left covariance and weak right covariance, then for all `a < b` and `c < d` in `α`, we have `a + c` < `b + d`.
|
Right.add_pos_of_nonneg_of_pos
theorem Right.add_pos_of_nonneg_of_pos :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α},
0 ≤ a → 0 < b → 0 < a + b
This theorem, `Right.add_pos_of_nonneg_of_pos`, asserts that for any type `α` that forms an `AddZeroClass` (i.e., it supports addition and has a zero element), is a `Preorder` (i.e., it has a binary relation that is reflexive and transitive), and has a right covariance property, if `a` and `b` are elements of `α` such that `a` is nonnegative (greater than or equal to zero) and `b` is positive (greater than zero), then the sum of `a` and `b` is also positive. This can be seen as a generalization of the property of real numbers where the sum of a nonnegative number and a positive number is always positive. The right covariance property in this context means that if `x` is less than or equal to `x_1`, then `y + x` is less than or equal to `y + x_1` for any `y`. A corresponding lemma for left covariance is `Left.add_pos_of_nonneg_of_pos`.
More concisely: If `α` is an AddZeroClass, Preorder type with right covariance property, and `a` is nonnegative and `b` is positive, then `a + b` is positive.
|
Right.one_lt_mul_of_le_of_lt
theorem Right.one_lt_mul_of_le_of_lt :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α},
1 ≤ a → 1 < b → 1 < a * b
The theorem `Right.one_lt_mul_of_le_of_lt` states that for any type `α` that is equipped with a multiplication operation, the operation to multiply by one element, and a preorder relationship (a binary relation that is reflexive and transitive), and assuming a right covariance (defined by the relation that the multiplication of two elements is less than or equal to the multiplication of two other elements), if `a` and `b` are two elements of this type such that `1 ≤ a` and `1 < b`, then it must be the case that `1 < a * b`. This theorem is a companion to the `Left.one_lt_mul_of_le_of_lt` theorem, which makes a similar claim under the assumption of left covariance.
More concisely: If `α` is a type with a multiplication operation, a preorder relation making it right covariant, and `1 ≤ a` and `1 < b` hold, then `1 < a * b`.
|
mul_lt_one'
theorem mul_lt_one' :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α}, a < 1 → b < 1 → a * b < 1
This theorem, named `mul_lt_one'`, states that for any type `α` that has both a multiplication operation and a `1` element (i.e., is a member of the `MulOneClass`), and also has a defined preorder (a relation that is reflexive and transitive), and that fulfills the `CovariantClass` condition (i.e., multiplication by a certain element preserves the order), then if two elements `a` and `b` of this type `α` are both less than `1`, their multiplication `a * b` is also less than `1`. The theorem assumes left covariance. There's a corresponding lemma that assumes right covariance named `Right.mul_lt_one'`.
More concisely: If `α` is a type with multiplication, a `1` element, a preorder satisfying the CovariantClass condition, and both `a` and `b` in `α` are less than `1`, then `a * b` is also less than `1`. (Assumes left covariance.)
|
mul_le_one'
theorem mul_le_one' :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α}, a ≤ 1 → b ≤ 1 → a * b ≤ 1
This theorem, named `mul_le_one'`, states that for any type `α` that is a multiplication one class and has a preorder, and is also covariant in a particular way, if `a` and `b` are two elements of `α` such that both `a` and `b` are less than or equal to 1, then the product of `a` and `b` is also less than or equal to 1. This theorem assumes left covariance. There is a corresponding lemma assuming right covariance, named `Right.mul_le_one`.
More concisely: If `α` is a multiplication one class with a preorder that is covariant in the left argument, then for all `a, b ∈ α` with `a ≤ 1` and `b ≤ 1`, we have `a * b ≤ 1`.
|
le_of_add_le_add_left
theorem le_of_add_le_add_left :
∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α]
[inst_2 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α},
a + b ≤ a + c → b ≤ c
This theorem, `le_of_add_le_add_left`, states that for any type `α` that has an addition operation, a "less than or equal to" relation, and is a contravariant class (meaning the sum of two elements is less than or equal to the sum of other two elements if and only if the first two elements are individually less than or equal to the other two elements); if the sum of `a` and `b` is less than or equal to the sum of `a` and `c`, then `b` is less than or equal to `c`. Essentially, it is a statement about the order preserving property of addition in a ordered semigroup.
More concisely: If `α` is a contravariant class with respect to addition and `a + b ≤ a + c` in `α`, then `b ≤ c`.
|
Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.29
theorem Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.29 :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_3 : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} (b : α),
(a + b < b) = (a < 0)
The theorem `Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.29` states that for all types `α`, given the type `α` is equipped with an additive zero class, less than relation, and the appropriate covariance and contravariance structures with respect to addition, then for all elements `a` and `b` of type `α`, `a + b` is less than `b` if and only if `a` is less than zero. In other words, in this specific algebraic structure, adding `b` to `a` only decreases the value of `b` if `a` is a negative value.
More concisely: For an additively commutative type equipped with an additive zero and a total order such that subtraction is the inverse operation to addition, if `a` and `b` are elements of this type and `a + b < b`, then `a < 0`.
|
mul_le_mul_iff_left
theorem mul_le_mul_iff_left :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a : α) {b c : α},
a * b ≤ a * c ↔ b ≤ c
This theorem, `mul_le_mul_iff_left`, states that for any type `α` that has multiplication and an order relation (denoted by `≤`), and that satisfies the `CovariantClass` and `ContravariantClass` properties with respect to multiplication and this order, for any elements `a`, `b`, and `c` of this type, the product of `a` and `b` is less than or equal to the product of `a` and `c` if and only if `b` is less than or equal to `c`. This can be interpreted as the order preservation property of multiplication when the multiplier is non-negative.
More concisely: For any type equipped with multiplication and a total order such that multiplication is covariant and contravariant with respect to the order, the product of two elements is less than or equal to the product of another pair if and only if the first pair is less than or equal to the second in the order.
|
Right.mul_lt_one
theorem Right.mul_lt_one :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b : α},
a < 1 → b < 1 → a * b < 1
This theorem, named `Right.mul_lt_one`, states that for any type `α` that has a multiplication and 'one' (as defined by the `MulOneClass`), and a less-than relation that is a preorder, and also satisfies right covariance (as specified by `CovariantClass` with `Function.swap`), if `a` and `b` are both less than `one`, then the product of `a` and `b` is also less than `one`. In other words, if we have two elements `a` and `b` of a ordered multiplicative structure (where multiplication is compatible with the order) and both are smaller than the multiplicative identity, their product is also smaller than the multiplicative identity.
More concisely: If `α` is an ordered multiplicative structure with one where multiplication is right-covariant and `a`, `b` are elements less than one, then `a * b` is also less than one.
|
add_pos'
theorem add_pos' :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, 0 < a → 0 < b → 0 < a + b
This theorem, referred to as `add_pos'`, states that for any type `α` that has properties of an additive zero class and a preorder, and for which addition is a covariant operation, if `a` and `b` are elements of `α` such that both `a` and `b` are greater than zero, then their sum `a + b` is also greater than zero. The conditions imposed on `α` ensure that it behaves like a number system with respect to addition, order, and the zero element.
More concisely: If `α` is an additive zero class and a preordered type with covariant addition, then for all `a, b ∈ α` with `a, b > 0`, we have `a + b > 0`.
|
MonotoneOn.mul_strictMono'
theorem MonotoneOn.mul_strictMono' :
∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {s : Set β}
[inst_3 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {f g : β → α},
MonotoneOn f s → StrictMonoOn g s → StrictMonoOn (fun x => f x * g x) s
This theorem states that if we have a set `s` of type `β`, and two functions `f` and `g` that map from `β` to `α`, where `α` is a type with a multiplication operation and a preorder relation, and if `f` is a monotone function on `s` and `g` is a strictly monotone function on `s`, then the function that maps every element `x` of `s` to the product of `f(x)` and `g(x)` is strictly monotone on `s`. Here, the property of being monotone means that if `a` and `b` are elements of `s` and `a ≤ b`, then `f(a) ≤ f(b)`, and being strictly monotone means that if `a < b`, then `f(a) < f(b)`. The type `α` is required to have certain additional properties related to the interaction of multiplication and the preorder relation.
More concisely: If `s` is a set with types `β`, `f` and `g` are monotone and strictly monotone functions respectively from `s` to a type `α` with a multiplication operation and a preorder relation such that `g` is strictly increasing, then the function `x => f x * g x` is strictly monotone on `s`.
|
mul_lt_mul_of_le_of_lt
theorem mul_lt_mul_of_le_of_lt :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b c d : α},
a ≤ b → c < d → a * c < b * d
The theorem `mul_lt_mul_of_le_of_lt` states that for any type `α` equipped with a multiplication operation, a preorder, and satisfying certain covariant properties, if `a` is less than or equal to `b` and `c` is less than `d` (`a ≤ b` and `c < d`), then the multiplication of `a` and `c` is less than the multiplication of `b` and `d` (`a * c < b * d`). This is a generalization of the property from real numbers where if you multiply a smaller number with another smaller number, the result is smaller than if you multiply the larger numbers.
More concisely: Given types `α` with a multiplication operation and a preorder, if `a ≤ b` and `c < d`, then `a * c < b * d`.
|
StrictMonoOn.mul_monotone'
theorem StrictMonoOn.mul_monotone' :
∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
[inst_3 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1],
StrictMonoOn f s → MonotoneOn g s → StrictMonoOn (fun x => f x * g x) s
The theorem states that if you have a function `f` that is strictly increasing on a set `s` (StrictMonoOn), and you have another function `g` that is non-decreasing (monotonic) on the same set `s` (MonotoneOn), then the function created by multiplying `f` and `g` at each point in `s` is also strictly increasing on `s`. This is under certain conditions which ensure that the multiplication operation is consistent with the orderings, i.e., if `x ≤ y` then `x * z ≤ y * z` and if `x < y` then `z * x < z * y` for any `z`.
More concisely: If `f` is strictly increasing and `g` is non-decreasing on a set `s`, then the function `x ↦ f x * g x` is strictly increasing on `s`, provided that multiplication is compatible with the orderings on `s`.
|
Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.27
theorem Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.27 :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α}, (a + b < a) = (b < 0)
This theorem states that, for any type `α` which has an additive zero element and a less-than relation, and is both covariant and contravariant for the addition operation and the less-than relation, for any elements `a` and `b` of this type, the statement "the sum of `a` and `b` is less than `a`" is equivalent to the statement "`b` is less than zero". That is, for given `a` and `b`, `a + b < a` if and only if `b < 0`.
More concisely: For any additive type `α` with a zero element and a negative element `−`, the equality `a + b < a` holds if and only if `b < −a`.
|
lt_add_of_lt_of_nonneg
theorem lt_add_of_lt_of_nonneg :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α},
b < c → 0 ≤ a → b < c + a
This theorem, `lt_add_of_lt_of_nonneg`, states that for any type `α` that has an addition operation and zero element (expressed by `AddZeroClass α`), and a preorder relation (expressed by `Preorder α`), and satisfies the `CovariantClass` property, if you have three elements `a`, `b`, and `c` such that `b` is less than `c` and `a` is non-negative (i.e., greater than or equal to zero), then `b` is less than the sum of `c` and `a`. In simpler terms, it says that adding a non-negative number to another number increases (or at least doesn't decrease) the value of the latter.
More concisely: If `α` is an additive preordered type with zero, and `a` is non-negative and `b` is less than `c`, then `b < c + a`.
|
lt_of_mul_lt_mul_left'
theorem lt_of_mul_lt_mul_left' :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : LT α]
[inst_2 : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b c : α},
a * b < a * c → b < c
This theorem, `lt_of_mul_lt_mul_left'`, asserts that for any type `α` equipped with a multiplication operation, a less-than relation, and a contravariant property between the multiplication and the less-than relation, if the product of `a` and `b` is less than the product of `a` and `c`, then `b` must be less than `c`. In other words, it allows us to infer inequality between two elements `b` and `c` from the inequality of their products with a common factor `a`, under certain algebraic assumptions. This theorem is a generalization of the familiar property from elementary algebra that if `a` is positive and `a * b < a * c`, then `b < c`.
More concisely: Given a type `α` with multiplication `*`, less-than relation `<`, and a contravariant property between multiplication and less-than, if `a * b < a * c`, then `b < c`.
|
add_nonneg
theorem add_nonneg :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, 0 ≤ a → 0 ≤ b → 0 ≤ a + b
The theorem `add_nonneg` states that for any type `α` that has an addition operation and a zero element (`AddZeroClass`), a preorder relation (`Preorder`), and is covariant in that adding an element to another increases its preorder value (`CovariantClass`), if `a` and `b` are elements of `α` and both are greater than or equal to zero, then their sum `a + b` is also greater than or equal to zero. This theorem is essentially an alias or a different name for the theorem `Left.add_nonneg`.
More concisely: For any type with an additive structure and a preorder relation that is covariant with respect to addition, if both operands are non-negative, then their sum is also non-negative.
|
MulLECancellable.mul_le_mul_iff_left
theorem MulLECancellable.mul_le_mul_iff_left :
∀ {α : Type u_1} [inst : LE α] [inst_1 : Mul α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b c : α},
MulLECancellable a → (a * b ≤ a * c ↔ b ≤ c)
The theorem `MulLECancellable.mul_le_mul_iff_left` states that for any type `α` that has a multiplication operation and a less than or equal to operation, and respects covariance under multiplication, given any three elements `a`, `b`, `c` of type `α`, if `a` is `MulLECancellable` (i.e., the function `x ↦ a * x` is order-reflecting), then the inequality `a * b ≤ a * c` is true if and only if `b ≤ c`. In simpler words, if `a` is `MulLECancellable`, then multiplying `a` with `b` or `c` doesn't change the order between `b` and `c`.
More concisely: For any type `α` with covariant multiplication and order `≤`, if `a` is `MulLECancellable,` then `a * b ≤ a * c` if and only if `b ≤ c.`
|
add_lt_add_of_lt_of_lt
theorem add_lt_add_of_lt_of_lt :
∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c d : α},
a < b → c < d → a + c < b + d
The theorem `add_lt_add_of_lt_of_lt` is a statement about an ordered, additive structure. It states that for any type `α` which has an addition operation and a preorder (a binary relation that is reflexive and transitive), and satisfies the covariance property with respect to addition and the less-than relation, if `a` is less than `b` and `c` is less than `d` (where `a`, `b`, `c`, and `d` are elements of `α`), then `a + c` is less than `b + d`. This is a version of the property that addition preserves order, which holds in many familiar ordered additive structures, like the natural numbers, integers, rationals, reals, etc.
More concisely: Given an additive preorder structure α with covariance property, if a < b and c < d, then a + c < b + d.
|
mul_lt_one_of_le_of_lt
theorem mul_lt_one_of_le_of_lt :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b : α}, a ≤ 1 → b < 1 → a * b < 1
This theorem, `mul_lt_one_of_le_of_lt`, is an alias of `Left.mul_lt_one_of_le_of_lt`. It asserts that, given any type `α` that is a multiplicative monoid and a preorder, and assuming left covariance, if `a` is a value of type `α` that is less than or equal to `1` and `b` is a value of `α` that is strictly less than `1`, then the product `a * b` is strictly less than `1`. The corresponding lemma for right covariance is `Right.mul_lt_one_of_le_of_lt`.
More concisely: If `α` is a multiplicative monoid with left covariance, and `a : α` is less than or equal to 1 and `b : α` is strictly less than 1, then `a * b` is strictly less than 1.
|
Monotone.add_strictMono
theorem Monotone.add_strictMono :
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {f g : β → α},
Monotone f → StrictMono g → StrictMono fun x => f x + g x
This theorem states that for any given types `α` and `β`, where `α` has an addition operation and both `α` and `β` have a preorder (i.e., they have a relation that is reflexive and transitive), and `α` has two covariant classes (which ensure that the addition operation preserves the respective orderings), if `f` and `g` are functions from `β` to `α` such that `f` is monotone (meaning that if `a ≤ b` then `f a ≤ f b`) and `g` is strictly monotone (meaning that if `a < b` then `f a < f b`), then the function that maps `x` to the sum of `f x` and `g x` is strictly monotone. In other words, the sum of a monotone function and a strictly monotone function is strictly monotone.
More concisely: If `α` is a type with an additive structure and a preorder, and `f` and `g` are functions from a preordered type `β` to `α`, with `f` monotone and `g` strictly monotone, then `x ≤ y` implies `f x + g x < f y + g y`.
|
Monotone.add_const
theorem Monotone.add_const :
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α}
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
Monotone f → ∀ (a : α), Monotone fun x => f x + a
The theorem `Monotone.add_const` states that for any types `α` and `β`, where `α` has an addition operation and both `α` and `β` are preordered, if a function `f` from `β` to `α` is monotone, then adding a constant `a` from `α` to the function `f` results in another monotone function. This is under the condition that `α` is a covariant class under the swap operation on addition and the less than or equal to relation. In simpler words, if you have a function that maintains order (monotone), then adding a constant to each output of that function still maintains the order (remains monotone).
More concisely: If `α` is a covariant preorder with respect to addition, and `f : β → α` is a monotone function, then `g : β → α` defined by `g(x) := f(x) + a` is also monotone for any constant `a ∈ α`.
|
Left.add_pos
theorem Left.add_pos :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α}, 0 < a → 0 < b → 0 < a + b
This theorem, `Left.add_pos`, states that for any type `α` that has an addition operation (`AddZeroClass α`), an order relation (`Preorder α`), and is left-covariant (`CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1`), if `a` and `b` are elements of this type such that `0 < a` and `0 < b`, then `0 < a + b`. In other words, in a left-covariant ordered additive structure, the sum of two positive elements is also positive.
More concisely: In a left-covariant ordered additive structure, the sum of two positive elements is positive.
|
Right.add_nonpos
theorem Right.add_nonpos :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α},
a ≤ 0 → b ≤ 0 → a + b ≤ 0
The theorem `Right.add_nonpos` states that for any type `α` that is an additive zero class and a preorder, and also satisfies the right covariance property, if `a` and `b` are elements of this type such that both `a` and `b` are less than or equal to zero, then their sum `a + b` is also less than or equal to zero. This theorem assumes right covariance, while there is a corresponding lemma that assumes left covariance named `Left.add_nonpos`.
More concisely: For any additive zero class and preorder type `α` satisfying right covariance, if `a` and `b` are its elements less than or equal to zero, then `a + b` is also less than or equal to zero.
|
lt_mul_of_le_of_one_lt
theorem lt_mul_of_le_of_one_lt :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b c : α},
b ≤ c → 1 < a → b < c * a
This theorem states that for any type `α` that has a multiplication and a one element (`MulOneClass`), and has a preorder relation (`Preorder`), and also satisfies the covariant property for multiplication and less than relation (`CovariantClass`), if `b` is less than or equal to `c` and `a` is more than one, then `b` is less than the product of `c` and `a`. In mathematical terms, given $b \leq c$ and $1 < a$ in this setting, we have $b < c \cdot a$.
More concisely: Given a type `α` with `MulOneClass`, `Preorder`, and `CovariantClass` structures, if `1 < a` and `b <= c`, then `b < c * a`.
|
le_mul_of_one_le_of_le
theorem le_mul_of_one_le_of_le :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b c : α},
1 ≤ a → b ≤ c → b ≤ a * c
The theorem `le_mul_of_one_le_of_le` states that for any type `α` that has multiplication and a one element (`MulOneClass`), a preorder relationship (transitivity and reflexivity), and is covariant (preserving order under multiplication), given any three elements `a`, `b`, and `c` of the type `α`, if `1` is less than or equal to `a`, and `b` is less than or equal to `c`, then `b` is less than or equal to the product of `a` and `c`. In other words, this theorem is about the order-preserving property of multiplication in a certain class of mathematical structures.
More concisely: If `α` is a type with multiplication, a one element `1`, a preorder relation that is transitive, reflexive, and covariant, then `1 ≤ a` and `b ≤ c` imply `b ≤ a * c`.
|
Left.one_lt_mul
theorem Left.one_lt_mul :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b : α}, 1 < a → 1 < b → 1 < a * b
This theorem, named `Left.one_lt_mul`, asserts that for any type `α` that has a multiplication operation and a preorder relation, and also satisfies the left covariance property (which essentially means multiplication preserves the order), if `a` and `b` are elements of `α` such that both `a` and `b` are greater than 1, then the product `a * b` is also greater than 1. The corresponding theorem for right covariance is `Right.one_lt_mul`.
More concisely: If `α` is a type with a multiplication operation and a preorder relation satisfying left covariance, and `a` and `b` are elements of `α` greater than 1, then `a * b` is also greater than 1.
|
Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.23
theorem Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.23 :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α},
(a < a + b) = (0 < b)
The theorem `Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.23` states that for any type `α` that is an additive zero class, has a less-than relation, and satisfies both the covariant and contravariant properties with respect to addition and the less-than relation, for any elements `a` and `b` of type `α`, `a` is less than `a` plus `b` if and only if zero is less than `b`. In other words, the increment of `a` by `b` results in a value greater than `a` if `b` is greater than zero.
More concisely: For any additive zero class type `α` with a total order relation satisfying covariance and contravariance properties with respect to addition, if `a` is less than `a + b`, then `0` is less than `b`.
|
StrictAnti.add
theorem StrictAnti.add :
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α}
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1],
StrictAnti f → StrictAnti g → StrictAnti fun x => f x + g x
The theorem `StrictAnti.add` states that the sum of two strictly antitone functions is also strictly antitone. In other words, if `f` and `g` are two functions from a set `β` to a set `α` such that for each pair of elements `a` and `b` in `β`, if `a < b` then `f(b) < f(a)` and `g(b) < g(a)`, then the function `h` defined by `h(x) = f(x) + g(x)` is also strictly antitone, i.e., if `a < b` then `h(b) < h(a)`. Here, `α` is a type with an addition operation and a preorder relation, while `β` is a type with a preorder relation.
More concisely: If `f` and `g` are strictly antitone functions from a preordered set `β` to an additively-structured, preordered set `α`, then their sum `h(x) = f(x) + g(x)` is also a strictly antitone function.
|
Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.15
theorem Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.15 :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α},
(a ≤ a + b) = (0 ≤ b)
This theorem is a lemma in the domain of algebraic order theory about monoids. It states that for all types 'α' that are instances of 'AddZeroClass' and 'LE', and satisfy both the 'CovariantClass' and 'ContravariantClass' for addition and less-than-or-equal-to operators, a given element 'a' of type 'α' is less than or equal to 'a' plus another element 'b' if and only if zero is less than or equal to 'b'. In other words, 'a' is less than or equal to its increment by 'b' exactly when 'b' is non-negative.
More concisely: For all types 'α' that are AddMonoids with respect to 'LE' and '+' operations, and are covariant and contravariant classes for '+' and "<=", we have a <= a + b if and only if 0 <= b.
|
le_add_of_nonneg_of_le
theorem le_add_of_nonneg_of_le :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α},
0 ≤ a → b ≤ c → b ≤ a + c
The theorem `le_add_of_nonneg_of_le` states that for all types `α` that have addition and zero, and are preordered (meaning they have a 'less than or equal to' relation that is transitive and reflexive), and for this 'less than or equal to' relation, it is covariant with respect to the operation of swap addition (i.e., if `x ≤ y` then `x + z ≤ y + z` for all `z`), given any three elements `a`, `b`, and `c` of type `α`, if `a` is greater than or equal to zero and `b` is less than or equal to `c`, then `b` is less than or equal to the sum of `a` and `c`. In simple terms, if `a` is non-negative and `b` is less than or equal to `c`, then `b` is less than or equal to `a + c`.
More concisely: If `α` is a type with addition, zero, and a preorder relation where the order is covariant with respect to addition, and `a ∈ α` is non-negative, `b, c ∈ α` are such that `b ≤ c`, then `b ≤ a + c`.
|
Left.mul_lt_one_of_lt_of_le
theorem Left.mul_lt_one_of_lt_of_le :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α}, a < 1 → b ≤ 1 → a * b < 1
This theorem states that for any type `α` which has multiplication and one as an identity (`MulOneClass`), has a total order (`Preorder`), and has left covariance, if `a` and `b` are elements of `α` such that `a` is less than one and `b` is less than or equal to one, then the product of `a` and `b` is less than one. The comment also indicates that there is a related lemma which assumes right covariance, named `Right.mul_lt_one_of_lt_of_le`.
More concisely: For any type `α` with multiplication, identity one, total order, and left covariance, if `a` is an element less than one and `b` is less than or equal to one, then `a * b` is less than one.
|
Left.add_pos_of_nonneg_of_pos
theorem Left.add_pos_of_nonneg_of_pos :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α}, 0 ≤ a → 0 < b → 0 < a + b
This theorem, `Left.add_pos_of_nonneg_of_pos`, states that for any type `α` that has an addition operation with a zero element (`AddZeroClass α`), a preorder relationship (`Preorder α`), and a left covariant property (`CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1`), if we have two elements `a` and `b` where `a` is non-negative (i.e., `0 ≤ a`) and `b` is positive (i.e., `0 < b`), then the sum `a + b` is also positive (`0 < a + b`). This is under the assumption of left covariance, and there is a corresponding lemma assuming right covariance named `Right.add_pos_of_nonneg_of_pos`.
More concisely: If `α` is a type with an additive structure, a preorder, and left covariance, and `a` is non-negative and `b` is positive, then `a + b` is positive.
|
StrictAntiOn.mul'
theorem StrictAntiOn.mul' :
∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
[inst_3 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1],
StrictAntiOn f s → StrictAntiOn g s → StrictAntiOn (fun x => f x * g x) s
This theorem states that the product of two strictly antitone functions is also strictly antitone. In other words, if `f` and `g` are two functions from a set `s` in `β` to `α`, such that both `f` and `g` are strictly antitone on `s` (i.e., for all `a, b` in `s`, if `a` is less than `b`, then `f(b)` is less than `f(a)` and `g(b)` is less than `g(a)`), then the function that maps `x` in `s` to `f(x)*g(x)` is also strictly antitone on `s`. This is under the assumptions that `α` is a type with multiplication and preorder (a binary relation that is reflexive and transitive) and that this multiplication operation is covariant, that is, increasing in both arguments.
More concisely: If `f` and `g` are strictly antitone functions from a preordered set `s` to a type `α` with covariant multiplication, then their product `x mapsto f(x) * g(x)` is also a strictly antitone function on `s`.
|
StrictMonoOn.mul'
theorem StrictMonoOn.mul' :
∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
[inst_3 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1],
StrictMonoOn f s → StrictMonoOn g s → StrictMonoOn (fun x => f x * g x) s
The theorem `StrictMonoOn.mul'` states that, given two functions `f` and `g` that map from a type `β` to a type `α`, and a set `s` of type `β`, under the conditions that `α` supports multiplication and has a preorder defined on it, and `β` has a preorder defined on it, if both `f` and `g` are strictly monotone on `s` (meaning that for any two elements `a` and `b` in `s`, if `a` is less than `b`, then `f(a)` is less than `f(b)` and `g(a)` is less than `g(b)`), then the function that maps each element `x` in `s` to `f(x) * g(x)` is also strictly monotone on `s`. This is additionally under the assumptions that multiplication on `α` is covariant (meaning that if `x` is less than `x_1`, then `x * y` is less than `x_1 * y`), and that the swap of multiplication on `α` is also covariant (meaning that if `x` is less than `x_1`, then `y * x` is less than `y * x_1`).
More concisely: If `f` and `g` are strictly monotone functions from a preordered set `β` to a multiplicatively preordered type `α`, then their pointwise product is also a strictly monotone function on `β`.
|
Left.one_lt_mul_of_le_of_lt
theorem Left.one_lt_mul_of_le_of_lt :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b : α}, 1 ≤ a → 1 < b → 1 < a * b
This theorem, `Left.one_lt_mul_of_le_of_lt`, states that for any type `α` that has a multiplication operation and a preorder relation (which is a relation that is reflexive and transitive), and also has a covariant class which allows multiplication of two elements in the type to be less than each other, if we have two elements `a` and `b` of the type `α` such that `1` is less than or equal to `a` and `1` is less than `b`, then `1` is less than the product of `a` and `b`. Basically, it provides a condition under which multiplication of two elements is guaranteed to result in a value larger than 1.
More concisely: Given types `α` with a preorder relation and a multiplication operation, if `1 ≤ a` and `1 < b`, then `1 < a * b`.
|
mul_lt_mul_of_lt_of_lt
theorem mul_lt_mul_of_lt_of_lt :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b c d : α},
a < b → c < d → a * c < b * d
The theorem `mul_lt_mul_of_lt_of_lt` states that for any type `α` equipped with a multiplication, a preorder, and satisfying two covariance conditions, if `a` and `b` are elements of `α` with `a < b`, and `c` and `d` are also elements of `α` with `c < d`, then the product `a * c` is less than the product `b * d`.
The two covariance conditions ensure that multiplication behaves well with the order: the first says that if `x < x_1` then `x * y < x_1 * y` for any `y`, and the second says that if `x < x_1` then `y * x < y * x_1` for any `y`. These conditions, along with the preorder structure, allow us to reason about the order of products in `α`.
More concisely: For any type `α` with a multiplication operation and a preorder satisfying the covariance conditions `x < x_1 → x * y < x_1 * y` and `x < x_1 → y * x < y * x_1`, if `a < b` and `c < d`, then `a * c < b * d`.
|
mul_eq_one_iff'
theorem mul_eq_one_iff' :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : PartialOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α},
1 ≤ a → 1 ≤ b → (a * b = 1 ↔ a = 1 ∧ b = 1)
The theorem `mul_eq_one_iff'` states that for any type `α` under the conditions that it has a multiplication and one (`MulOneClass α`), it has a partial order (`PartialOrder α`), and this type `α` is covariant in both the multiplication operation (`fun x x_1 => x * x_1`) and its swapped version (`Function.swap fun x x_1 => x * x_1`) with respect to the partial order (`fun x x_1 => x ≤ x_1`), then for any two elements `a` and `b` of this type, if `a` and `b` are both greater than or equal to one (`1 ≤ a` and `1 ≤ b`), the product `a * b` is equal to one (`a * b = 1`) if and only if both `a` and `b` are equal to one (`a = 1` and `b = 1`). This theorem essentially asserts a property of multiplication relative to the multiplicative identity in a partially ordered monoid that is covariant under multiplication.
More concisely: Given a type `α` with multiplication `*`, one (`1`), partial order `≤`, and covariance under multiplication, if `a, b ∈ α` satisfy `1 ≤ a` and `1 ≤ b`, then `a * b = 1` if and only if `a = b = 1`.
|
Right.add_lt_add
theorem Right.add_lt_add :
∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c d : α},
a < b → c < d → a + c < b + d
The theorem `Right.add_lt_add` asserts that for any type `α` equipped with an addition operation, a preorder (a reflexive and transitive relation), and satisfying two covariance properties, whenever `a < b` and `c < d` for any `a`, `b`, `c`, and `d` of type `α`, we have `a + c < b + d`. The two covariance properties required are: the sum of two elements is larger if the first element is larger (`inst_2`), and the sum of two elements is strictly larger if the second element is strictly larger when their order is swapped (`inst_3`).
More concisely: Given a type `α` with an addition operation and a preorder, if the sum of two elements is larger when the first is larger (inst_2) and strictly larger when the second is strictly larger when their order is swapped (inst_3), then for any `a < b` and `c < d` in `α`, we have `a + c < b + d`.
|
add_lt_add_iff_left
theorem add_lt_add_iff_left :
∀ {α : Type u_1} [inst : Add α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b c : α},
a + b < a + c ↔ b < c
This theorem, `add_lt_add_iff_left`, states that for any type `α` that supports addition (`Add α`) and a less than operation (`LT α`), given certain covariance and contravariance conditions, for any three elements `a`, `b`, and `c` of this type, the inequality `a + b < a + c` is equivalent to `b < c`. Essentially, it says that if adding `a` to two other numbers results in one sum being less than the other, then it must be the case that the original numbers were also in the same less than relationship.
More concisely: For types `α` with addition and less than relations, `a + b < a + c` if and only if `b < c`.
|
le_mul_of_one_le_right'
theorem le_mul_of_one_le_right' :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α}, 1 ≤ b → a ≤ a * b
This theorem, named `le_mul_of_one_le_right'`, asserts that in a type `α` that is a multiplication one-class and has a less than or equal to (`LE`) relation, if the multiplication operation is covariant and if `1` is less than or equal to some value `b`, then any value `a` of the type is less than or equal to the product of `a` and `b`. Thus, when `b` is greater than or equal to `1`, multiplying `a` by `b` will not make the product smaller than `a`.
More concisely: If `α` is a multiplication one-class with `LE` relation, `1 ≤ b`, and multiplication is covariant in the first argument, then for all `a ∈ α`, we have `a ≤ a * b`.
|
add_lt_add_of_le_of_lt
theorem add_lt_add_of_le_of_lt :
∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c d : α},
a ≤ b → c < d → a + c < b + d
This theorem, named `add_lt_add_of_le_of_lt`, states that for all types `α` equipped with an additive operation, a preorder (an ordering relation that is reflexive and transitive), and two covariant classes (that ensure compatibility between the additive operation and the ordering relations), given four elements `a`, `b`, `c`, and `d` of type `α`, if `a` is less than or equal to `b` and `c` is strictly less than `d`, then the sum of `a` and `c` is strictly less than the sum of `b` and `d`. In other words, if `a ≤ b` and `c < d`, then `a + c < b + d`.
More concisely: For all types `α` with additive operation, preorder, and covariant classes: if `a ≤ b` and `c < d` in `α`, then `a + c < b + d`.
|
AntitoneOn.add
theorem AntitoneOn.add :
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
AntitoneOn f s → AntitoneOn g s → AntitoneOn (fun x => f x + g x) s
This theorem states that the sum of two antitone functions is also antitone. Given two functions `f` and `g` from a set `s` of type `β` to a type `α` that has an addition operation and a preorder relation, if both `f` and `g` are antitone on `s`, meaning that for all `a, b ∈ s`, `a ≤ b` implies `f b ≤ f a` and `g b ≤ g a` respectively, then the function defined by `(fun x => f x + g x)` is also antitone on `s`. This is under the condition that `α` is a covariant class under the addition operation and the preorder relation, both in the original order and when the arguments to addition are swapped.
More concisely: If `f` and `g` are antitone functions from a preordered set `(s, ≤)` to a covariant additive preordered set `(α, ≤)`, then their sum `(fun x => f x + g x)` is also an antitone function on `s`.
|
Left.mul_lt_one
theorem Left.mul_lt_one :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b : α}, a < 1 → b < 1 → a * b < 1
This theorem, `Left.mul_lt_one`, declares that for any type `α` equipped with multiplication, an identity element (making it a `MulOneClass`), and a preorder relation, and assuming left covariance, if `a` and `b` are elements of `α` such that both `a` and `b` are less than 1, then the product `a * b` is also less than 1.
More concisely: For any type `α` with multiplication, an identity element, and a preorder relation, if `a` and `b` are elements of `α` with `0 < a` and `0 < b`, then `0 < a * b` (assuming left covariance).
|
Monotone.mul'
theorem Monotone.mul' :
∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α}
[inst_3 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1],
Monotone f → Monotone g → Monotone fun x => f x * g x
The theorem 'Monotone.mul'' states that for any type `α` with multiplication and preorder relations, and any type `β` with a preorder relation, if functions `f` and `g` are both monotone from `β` to `α` and `α` is covariant in both its multiplication function and its swapped multiplication function with respect to preorder, then the function that maps each `x` in type `β` to the product of `f(x)` and `g(x)` is also monotone. In other words, the product of two monotone functions is itself monotone under these conditions.
More concisely: If `α` is a type with covariant multiplication and `β` is a type with a preorder relation, and `f` and `g` are monotone functions from `β` to `α`, then the function mapping `x` to `f(x) * g(x)` is monotone.
|
Right.mul_lt_one_of_le_of_lt
theorem Right.mul_lt_one_of_le_of_lt :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α},
a ≤ 1 → b < 1 → a * b < 1
This theorem, named `Right.mul_lt_one_of_le_of_lt`, makes assumptions on the type `α` such that it has a multiplication and a one element (with `MulOneClass α`), a preorder structure (with `Preorder α`), and a right covariance property (with `CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1`). Given these conditions, for any two instances `a` and `b` of `α`, if `a` is less than or equal to 1 (`a ≤ 1`) and `b` is less than 1 (`b < 1`), then the product `a * b` is less than 1 (`a * b < 1`). The analogous theorem assuming left covariance is `Left.mul_lt_one_of_le_of_lt`.
More concisely: Given an type `α` with multiplication, one element, preorder structure, and right covariance, if `a` and `b` are elements of `α` with `a ≤ 1` and `b < 1`, then `a * b < 1`.
|
Right.add_nonneg
theorem Right.add_nonneg :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α},
0 ≤ a → 0 ≤ b → 0 ≤ a + b
This theorem, referred to as `Right.add_nonneg`, states that for any type `α` that has the structure of an additive zero class and a preorder and obeys the right covariance property, if `a` and `b` are elements of type `α` and both are greater than or equal to zero, then the sum of `a` and `b` is also greater than or equal to zero.
The right covariance is captured by the `CovariantClass` instance, where the order-preserving function is the addition (`fun x x_1 => x + x_1`) after swapping the arguments (`Function.swap`), and the order relation is `≤`. This theorem is the counterpart to another lemma that assumes left covariance, referred to as `Left.add_nonneg`.
More concisely: For any additive zero class type `α` with right covariance, if `a` and `b` are non-negative elements, then `a + b` is also non-negative.
|
add_le_add_iff_right
theorem add_le_add_iff_right :
∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) {b c : α},
b + a ≤ c + a ↔ b ≤ c
The theorem `add_le_add_iff_right` states that for all types `α` equipped with addition, a less-than-or-equal-to order that obeys both the covariant and contravariant properties, and any elements `a`, `b`, and `c` of type `α`, the inequality `b + a ≤ c + a` holds if and only if `b ≤ c`. In other words, in this ordered additive structure, adding the same element `a` to both sides of an inequality does not change the inequality's validity.
More concisely: For all types `α` with covariant and contravariant additions and order `≤`, if `a`, `b`, and `c` are elements of `α`, then `b + a ≤ c + a` if and only if `b ≤ c`.
|
Left.one_lt_mul'
theorem Left.one_lt_mul' :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α}, 1 < a → 1 < b → 1 < a * b
This theorem, `Left.one_lt_mul'`, states that for any type `α` that is a multiplication class with a one element, and also a preorder, and if multiplication on `α` is left-covariant, then for any two elements `a` and `b` of `α`, if both `a` and `b` are greater than one, their multiplication `a * b` is also greater than one. In other words, in a context where multiplication preserves order from the left, the product of two numbers greater than one is also greater than one. The corresponding theorem for right covariance is `Right.one_lt_mul'`.
More concisely: If `α` is a preorder type with a one element and left-covariant multiplication, then for all `a`, `b` in `α` with `a * b` defined and `a`, `b` > 1, it follows that `a * b` > 1.
|
Right.add_neg_of_neg_of_nonpos
theorem Right.add_neg_of_neg_of_nonpos :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α},
a < 0 → b ≤ 0 → a + b < 0
This theorem, `Right.add_neg_of_neg_of_nonpos`, is about an algebraic structure with an addition operation and a zero element (expressed by the `AddZeroClass`), and a preorder relation (expressed by `Preorder`). It also assumes right-covariance (`CovariantClass`) for the addition operation.
The theorem states that for any two elements `a` and `b` in this structure, if `a` is less than zero and `b` is less than or equal to zero, then the sum of `a` and `b` is also less than zero. This expresses a specific property about the interaction between addition and the preorder in this structure.
More concisely: If `a` and `b` are elements in an additive structure with a preorder relation and right-covariance, where `a` is negative and `b` is less than or equal to zero, then `a + b` is negative.
|
add_lt_of_neg_of_le
theorem add_lt_of_neg_of_le :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α},
a < 0 → b ≤ c → a + b < c
The theorem `add_lt_of_neg_of_le` states that for all types `α` that are an instance of the `AddZeroClass`, `Preorder`, and have a `CovariantClass` with the specified properties, if a number `a` is less than zero and another number `b` is less than or equal to `c`, then the sum of `a` and `b` is less than `c`. The `CovariantClass` condition ensures that the addition operation respects the ordering `<` on the type `α`.
More concisely: For all types `α` with `AddZeroClass`, `Preorder`, and covariant additions, if `a < 0` and `b <= c`, then `a + b < c`.
|
one_le_mul
theorem one_le_mul :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α}, 1 ≤ a → 1 ≤ b → 1 ≤ a * b
This theorem, named `one_le_mul`, states that for any type `α` that has the characteristics of a `MulOneClass` (a structure with multiplication and a unique 1 element) and a `Preorder` (a structure with a reflexive and transitive binary relation), and that satisfies the `CovariantClass` property (the relation remains invariant when both arguments are transformed by the same function), if `a` and `b` are elements of `α` such that both are greater than or equal to 1, then their product `a * b` is also greater than or equal to 1. The theorem assumes left covariance; there is a parallel theorem `Right.one_le_mul` that assumes right covariance.
More concisely: For any type `α` with Multiplicative Identity `1` and a Preorder relation that is covariant, if `a` and `b` are elements greater than or equal to `1`, then their product `a * b` is also greater than or equal to `1`.
|
MonotoneOn.mul'
theorem MonotoneOn.mul' :
∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
[inst_3 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1],
MonotoneOn f s → MonotoneOn g s → MonotoneOn (fun x => f x * g x) s
This theorem states that the product of two monotone functions is also monotone. More specifically, for all types `α` and `β` with multiplication and preorder operations, if `f` and `g` are two functions from `β` to `α` defined on a set `s` of `β`, and both `f` and `g` are monotone on `s` (i.e., for all `a, b` in `s`, `a ≤ b` implies `f(a) ≤ f(b)` and `g(a) ≤ g(b)`), then the function that maps `x` in `s` to `f(x) * g(x)` is also monotone on `s`. This means that if `a, b` are in `s` and `a ≤ b`, then `f(a) * g(a) ≤ f(b) * g(b)`. The conditions `CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1` and `CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1` are technical conditions needed to make the multiplication and comparison operations interact correctly.
More concisely: If `f` and `g` are two monotonic functions from a preordered set `(β, ≤)` to a commutative monoid `(α, *),` then their product `h(x) = f(x) * g(x)` is also a monotonic function on `β.`
|
Right.one_lt_mul
theorem Right.one_lt_mul :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b : α},
1 < a → 1 < b → 1 < a * b
The theorem `Right.one_lt_mul` states that for any type `α` that has a multiplication and identity element (`MulOneClass α`), an ordering (`Preorder α`), and is right-covariant (meaning that multiplication on the right by a greater element yields a greater result), if `a` and `b` are elements of `α` such that both `a` and `b` are greater than the identity element `1`, then their product `a * b` is also greater than `1`. In simpler terms, if you have two numbers greater than one, their product is also greater than one, under the assumptions of right covariance.
More concisely: If `α` is a type with multiplication, identity element, ordering, and right-covariance such that `a` and `b` are greater than the identity element `1`, then `a * b` is greater than `1`.
|
Monotone.const_mul'
theorem Monotone.const_mul' :
∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α}
[inst_3 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1],
Monotone f → ∀ (a : α), Monotone fun x => a * f x
The theorem 'Monotone.const_mul'' states that for all types 'α' and 'β' with 'α' being a multiplication and preorder structure and 'β' being a preorder structure, given a function 'f' from 'β' to 'α', if 'f' is a monotone function and 'a' is an element of type 'α', then the function that takes 'x' to 'a * f x' is also a monotone function. This implies that multiplication by a constant preserves the monotonicity of a function.
More concisely: If f is a monotone function from a preorder (β) to a multiplication and preorder structure (α), then the function x ↔-> a * f x is also monotone.
|
lt_add_of_nonneg_of_lt
theorem lt_add_of_nonneg_of_lt :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α},
0 ≤ a → b < c → b < a + c
The theorem `lt_add_of_nonneg_of_lt` states that for any type `α` which has an addition operation, zero element (is an `AddZeroClass`), and has a preorder relation (is a `Preorder`), and the addition operation is covariant (satisfies the `CovariantClass` property), if `a`, `b`, and `c` are elements of `α` such that `a` is nonnegative (i.e., `0 ≤ a`) and `b` is less than `c` (i.e., `b < c`), then `b` is also less than the sum of `a` and `c` (i.e., `b < a + c`). This is a statement about the order-preserving nature of addition when one of the added values is nonnegative.
More concisely: If `α` is a type with Addition, Zero, Preorder, and Covariant properties, and `0 ≤ a` and `b < c` in `α`, then `b < a + c`.
|
add_pos_of_pos_of_nonneg
theorem add_pos_of_pos_of_nonneg :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, 0 < a → 0 ≤ b → 0 < a + b
The theorem `add_pos_of_pos_of_nonneg` states that for any type `α` that has the structure of an `AddZeroClass` and a `Preorder`, and satisfies the `CovariantClass` properties (essentially, these properties state that addition and the order relation interact in a specific, 'nice' way), if `a` and `b` are elements of `α` such that `a` is strictly greater than zero and `b` is nonnegative (greater than or equal to zero), then the sum of `a` and `b` is strictly greater than zero.
More concisely: If `α` is a type with `AddZeroClass` and `Preorder` structures satisfying covariance properties, and `a` is strictly positive and `b` is nonnegative in `α`, then `a + b` is strictly positive.
|
Antitone.mul_strictAnti'
theorem Antitone.mul_strictAnti' :
∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {f g : β → α},
Antitone f → StrictAnti g → StrictAnti fun x => f x * g x
The theorem `Antitone.mul_strictAnti'` states that for any types `α` and `β`, given multiplication on `α` and `α` and `β` having a preorder structure, if `α` has a covariant class under multiplication that respects the less than relationship, and `α` has a covariant class under swapped multiplication that respects the less than or equal relationship, then given any two functions `f` and `g` from `β` to `α` where `f` is antitone (meaning `f` preserves the reversed order) and `g` is strictly antitone (meaning `g` strictly preserves the reversed order), the function that maps `x` in `β` to the product of `f(x)` and `g(x)` in `α` is also strictly antitone.
More concisely: If types `α` and `β` have preorders, `α` has covariant classes for multiplication and swapped multiplication respecting the lesser-than relation and less-than-or-equal relation respectively, and `f` is antitone and `g` is strictly antitone from `β` to `α`, then the function `x ↦ f(x) * g(x)` from `β` to `α` is strictly antitone.
|
StrictAnti.add_antitone
theorem StrictAnti.add_antitone :
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α}
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1],
StrictAnti f → Antitone g → StrictAnti fun x => f x + g x
The theorem `StrictAnti.add_antitone` states that for any two functions `f` and `g` that map from a type `β` to a type `α`, such that `α` has an addition operation and preorders exists for both `α` and `β`, and additionally, if `α` has a left-covariant class for addition and inequality, and a right-covariant class for addition and strict inequality, then if `f` is strictly antitone (meaning for all `a` and `b` in `α`, if `a < b` then `f(b) < f(a)`) and `g` is antitone (meaning for all `a` and `b` in `α`, if `a ≤ b` then `g(b) ≤ g(a)`), the sum of `f` and `g` is also strictly antitone. This means that for all `x` and `y` in `β`, if `x < y` then `f(y) + g(y) < f(x) + g(x)`.
More concisely: If `α` is a type with an addition operation, preorders, and covariant classes for addition and strict inequality, and `f : β -> α` is strictly antitone and `g : β -> α` is antitone, then `f + g : β -> α` is strictly antitone. (That is, for all `x` and `y` in `β`, `x < y` implies `f(y) + g(y) < f(x) + g(x)`.)
|
le_of_add_le_add_right
theorem le_of_add_le_add_right :
∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α]
[i : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α},
b + a ≤ c + a → b ≤ c
The theorem `le_of_add_le_add_right` states that for all types `α` equipped with an addition operator and a less-than-or-equal-to relation, and for which the less-than-or-equal-to relation is contravariant with respect to swapping the arguments of the addition operation, if `b + a` is less than or equal to `c + a` for any elements `a`, `b`, and `c` of type `α`, then `b` must be less than or equal to `c`. This essentially captures the intuitive property of "cancelling" the same quantity from both sides of an inequality.
More concisely: If for all `α` with addition and `≤` such that `≤` is contravariant, `a ≤ b` implies `a + c ≤ b + c` for all `a, b, c` in `α`, then `b ≤ c`.
|
add_eq_zero_iff'
theorem add_eq_zero_iff' :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : PartialOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α},
0 ≤ a → 0 ≤ b → (a + b = 0 ↔ a = 0 ∧ b = 0)
The theorem `add_eq_zero_iff'` states that for any type `α` that is a member of the `AddZeroClass` (indicating it has addition and zero operations), has a partial order, and is covariant with regards to addition and order, if `a` and `b` are two elements of `α` such that `0 ≤ a` and `0 ≤ b`, then the sum `a + b` equals zero if and only if `a` and `b` are both zero. In simpler terms, in this particular structure, the only way for the sum of two non-negative elements to be zero is if both elements are zero themselves.
More concisely: For any type `α` in Lean 4 that is an AddMonoid with zero, has a partial order, and is covariant with respect to both addition and order, `0 ≤ a` and `0 ≤ b` imply `a + b = 0` if and only if `a = b = 0`.
|
Monotone.add
theorem Monotone.add :
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α}
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
Monotone f → Monotone g → Monotone fun x => f x + g x
The theorem `Monotone.add` asserts that if you have two monotone functions, `f` and `g`, which map from a type `β` to a type `α`, where `α` is an additive preorder and `β` is a preorder, then the function that maps each element in `β` to the sum of `f` and `g` applied to that element is also monotone. This holds under the conditions that `α` is a covariant class under addition and ordering, and also under addition and ordering after swapping the arguments.
More concisely: If `f` and `g` are monotone functions from a preordered type `β` to an additively ordered type `α`, then the function `x ↔ f x + g x` is monotone.
|
Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.8
theorem Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.8 :
∀ {α : Type u_1} [inst : Add α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_3 : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b c : α},
(b + a < c + a) = (b < c)
The theorem `Mathlib.Algebra.Order.Monoid.Lemmas._auxLemma.8` states that for all types `α` that have an addition operation and a less-than relation, provided they satisfy both a CovariantClass property and a ContravariantClass property with respect to a `Function.swap` operation on addition and less-than, for any terms `a`, `b`, and `c` of type `α`, the relation `(b + a < c + a) = (b < c)` holds. In simpler terms, this theorem is about the cancellation property in ordered monoids: if you add the same term `a` to two terms `b` and `c`, the inequality between `b` and `c` does not change.
More concisely: In an ordered monoid, swapping the order of adding a term to two other terms preserves the inequality between them: i.e., for all `α` with CovariantClass and ContravariantClass structures, `(b < c) = (b + a < c + a)` for any `a, b, c` in `α`.
|
AntitoneOn.add_strictAnti
theorem AntitoneOn.add_strictAnti :
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {s : Set β}
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {f g : β → α},
AntitoneOn f s → StrictAntiOn g s → StrictAntiOn (fun x => f x + g x) s
This theorem asserts that if you have a set `s` of elements of type `β` and two functions `f` and `g` mapping from `β` to `α`, where `α` is a type with an addition operation and an order, then if `f` is an antitone function on `s` (meaning that it preserves the order of the elements in the opposite direction: for any `a` and `b` in `s`, if `a ≤ b` then `f(b) ≤ f(a)`) and `g` is strictly antitone on `s` (that is, it strictly preserves the order in the opposite direction: for any `a` and `b` in `s`, if `a < b` then `f(b) < f(a)`), then the function that maps each element `x` of `s` to `f(x) + g(x)` is also strictly antitone on `s`. This property holds under some conditions on the order and addition of `α`: the addition of `α` is both strictly and non-strictly monotone, meaning that increasing one of the operands either strictly or non-strictly increases the result.
More concisely: If `s` is a set of elements from type `β`, `f` is an antitone function and `g` is a strictly antitone function on `s` with values in the additive semigroup `α` where addition is both strictly and non-strictly monotone, then the function that maps each element `x` in `s` to `f(x) + g(x)` is strictly antitone on `s`.
|
Right.mul_lt_one_of_lt_of_le
theorem Right.mul_lt_one_of_lt_of_le :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b : α},
a < 1 → b ≤ 1 → a * b < 1
This theorem, named `Right.mul_lt_one_of_lt_of_le`, asserts that for any type `α` that has a multiplication operation and a one element, a preorder relation, and satisfies the right covariance property (which means that if `x < y`, then `z * x < z * y` for all `z`), if `a` and `b` are elements of this type such that `a` is less than `1` and `b` is less than or equal to `1`, then the product of `a` and `b` is less than `1`. The relation is assumed to be right covariant, meaning it preserves order under multiplication from the right. There is a corresponding theorem for left covariance, named `Left.mul_lt_one_of_lt_of_le`.
More concisely: If `α` is a type with multiplication, one element, preorder relation respecting right covariance, and `a` and `b` are elements with `0 < a` and `0 <= b`, then `a * b < 1`.
|
StrictMono.add
theorem StrictMono.add :
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α}
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1],
StrictMono f → StrictMono g → StrictMono fun x => f x + g x
The theorem `StrictMono.add` states that given two functions `f` and `g` from a preordered type `β` to an additively preordered type `α`, if both `f` and `g` are strictly monotone (i.e., if for all pairs of elements `a` and `b` in `β` such that `a < b`, we have both `f(a) < f(b)` and `g(a) < g(b)`), then the function that maps each element `x` of `β` to the sum `f(x) + g(x)` is also strictly monotone. This statement requires that addition on `α` is compatible with the preorder, both in the original order and in the reverse order.
More concisely: If `f` and `g` are strictly monotone functions from a preordered type `β` to an additively preordered type `α` such that addition on `α` respects the preorder in both forward and reverse directions, then the function `x => f(x) + g(x)` is strictly monotone.
|
le_add_iff_nonneg_right
theorem le_add_iff_nonneg_right :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α},
a ≤ a + b ↔ 0 ≤ b
This theorem, `le_add_iff_nonneg_right`, states that for all elements `a` and `b` in a type `α` that has an addition operation and a less than or equal to order (`LE`), it holds that `a` is less than or equal to `a + b` if and only if `0` is less than or equal to `b`. The type `α` must be equipped with an `AddZeroClass` instance, meaning it has a zero element and an addition operation. Additionally, the type `α` needs to have the properties of `CovariantClass` and `ContravariantClass` with respect to addition and the order, meaning that the order and the addition operation interact in certain specific ways.
More concisely: For all elements `a` in a type `α` with addition and order, `a ≤ a + b` if and only if `0 ≤ b`.
|
Left.add_neg_of_nonpos_of_neg
theorem Left.add_neg_of_nonpos_of_neg :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α}, a ≤ 0 → b < 0 → a + b < 0
This theorem is named `Left.add_neg_of_nonpos_of_neg` and it states that for any type `α` that has the properties of an additive zero class and a preorder, and is left-covariant, given two elements `a` and `b` of this type, if `a` is less than or equal to zero and `b` is less than zero, then the sum of `a` and `b` is less than zero. It should be noted that this theorem assumes left covariance, and there is a corresponding lemma for right covariance named `Right.add_neg_of_nonpos_of_neg`.
More concisely: For any additive zero class and preordered type `α` that is left-covariant, if `a` and `b` are elements of `α` with `a ≤ 0` and `b < 0`, then `a + b < 0`.
|
add_neg'
theorem add_neg' :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, a < 0 → b < 0 → a + b < 0
The theorem `add_neg'` states that for any type `α` that has a `AddZeroClass` instance (meaning it has addition and a zero element), a `Preorder` instance (meaning it has an ordering that is reflexive and transitive), and a `CovariantClass` instance (which means that it behaves nicely with respect to the addition and the ordering), if two elements `a` and `b` of this type are both less than zero, then their sum `a + b` is also less than zero. It's essentially saying that the sum of two negative numbers in an ordered additive group is still negative.
More concisely: If `α` is an additive group with a total ordering such that both `a` and `b` are negative elements of `α`, then `a + b` is also negative.
|
Left.add_neg
theorem Left.add_neg :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α}, a < 0 → b < 0 → a + b < 0
This theorem, `Left.add_neg`, states that for any type `α` that is an instance of the `AddZeroClass`, `Preorder`, and satisfies the left covariance property, if `a` and `b` are elements of type `α` and both are less than zero, then the sum of `a` and `b` is also less than zero. In mathematical terms, it means that for a preordered additive group, the sum of two negative elements is also negative.
More concisely: For any additive group `α` with a preorder relation making it a left covariant add monoid, if `a` and `b` are negative elements of `α`, then `a + b` is also negative.
|
le_add_of_nonneg_right
theorem le_add_of_nonneg_right :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, 0 ≤ b → a ≤ a + b
This theorem states that for any type `α` that has an addition operation (`AddZeroClass α`) and a less than or equal to operation (`LE α`), and for this addition operation, if `x + y1` is less than or equal to `x + y2` whenever `y1` is less than or equal to `y2` (`CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1`), then for any two elements `a` and `b` of this type, if `b` is nonnegative (i.e., `0 ≤ b`), then `a` is less than or equal to `a + b`. In other words, adding a nonnegative number to a number will result in a number that is greater than or equal to the original number.
More concisely: If `α` is a type with `AddZeroClass` and `LE`, and ` CovariantClass` holds for addition and the `LE` relation, then for all `a` and non-negative `b` in `α`, we have `a ≤ a + b`.
|
AddLECancellable.Injective
theorem AddLECancellable.Injective :
∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] {a : α},
AddLECancellable a → Function.Injective fun x => a + x
The theorem `AddLECancellable.Injective` states that for any type `α` that supports addition operation and partial order, given any element `a` of type `α`, if `a` is left addition-cancellable (meaning that for all elements `b` and `c` of type `α`, `a + b ≤ a + c` implies `b ≤ c`), then the function that adds `a` to its argument is injective. An injective function is one where different inputs yield different outputs, i.e., if `f(x) = f(y)`, then `x = y`. In simpler terms, if adding `a` doesn't change the order of elements, then adding `a` to different elements will give different results.
More concisely: If `α` is a type with additions and a partial order such that every left additive cancellative element `a` implies the function `x => a + x` is injective.
|
one_lt_mul_of_le_of_lt'
theorem one_lt_mul_of_le_of_lt' :
∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b : α}, 1 ≤ a → 1 < b → 1 < a * b
This theorem, `one_lt_mul_of_le_of_lt'`, states that for any type `α` that has a multiplicative structure with identity (`MulOneClass α`), an order relation (`Preorder α`), and satisfies a left covariance property (`CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1`), if `a` and `b` are elements of `α` such that `1` is less than or equal to `a` and `1` is strictly less than `b`, then `1` is strictly less than the product of `a` and `b`. This theorem is an alias of `Left.one_lt_mul_of_le_of_lt` and assumes left covariance. There is a corresponding lemma that assumes right covariance, `Right.one_lt_mul_of_le_of_lt`.
More concisely: If `α` is a type with a multiplicative structure, order relation, and left covariance, and `1` is less than or equal to `a` and strictly less than `b`, then `1` is strictly less than `a * b`.
|
mul_lt_mul_iff_left
theorem mul_lt_mul_iff_left :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
[inst_3 : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] (a : α) {b c : α},
a * b < a * c ↔ b < c
This theorem, `mul_lt_mul_iff_left`, states that for any type `α` which supports multiplication (`Mul α`) and less than operation (`LT α`) and follows certain mathematical properties (`CovariantClass` and `ContravariantClass`), the product `a * b` is less than `a * c` if and only if `b` is less than `c`. This is assuming that `a`, `b`, and `c` are all of type `α`. In other words, it states that multiplying both sides of a strict inequality by the same positive number doesn't affect the inequality's direction.
More concisely: For all types `α` with multiplication and less-than relations that are covariant and contravariant, `a * b` is less than `a * c` if and only if `b` is less than `c`.
|
le_of_mul_le_mul_left'
theorem le_of_mul_le_mul_left' :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : LE α]
[inst_2 : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b c : α},
a * b ≤ a * c → b ≤ c
This theorem, `le_of_mul_le_mul_left'`, states that for any type `α` that has a multiplication operation, an order (less than or equal to), and the order is contravariant in the multiplication (meaning that if `x * y` decreases then `x` decreases for any `y`), if the product of `a` and `b` is less than or equal to the product of `a` and `c`, then `b` is less than or equal to `c`. This essentially captures the property in arithmetic that if `a * b` is less than `a * c` (and `a` is not zero), then `b` must be less than `c`.
More concisely: If `α` is a type with contravariant order and multiplication, and `a * b ≤ a * c`, then `b ≤ c`.
|
mul_lt_mul_of_lt_of_le
theorem mul_lt_mul_of_lt_of_le :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b c d : α},
a < b → c ≤ d → a * c < b * d
The theorem `mul_lt_mul_of_lt_of_le` states that, for all elements `a`, `b`, `c`, and `d` of a type `α` that is equipped with a multiplication operation, a preorder (reflexive and transitive binary relation), and satisfies two covariant class conditions on multiplication (one for the relation `≤` and another for the relation `<` swapped), if `a` is less than `b` and `c` is less than or equal to `d`, then the product `a * c` is less than the product `b * d`. This theorem captures a multiplicative property of ordered structures.
More concisely: For all types `α` equipped with a multiplication operation and a preorder `≤` satisfying certain covariant conditions, if `a ≤ b` and `c ≤ d`, then `a * c ≤ b * d`.
|
StrictAntiOn.add
theorem StrictAntiOn.add :
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1],
StrictAntiOn f s → StrictAntiOn g s → StrictAntiOn (fun x => f x + g x) s
The theorem `StrictAntiOn.add` states that for any set `s` and any types `α` and `β` where `α` is an additive preorder that is covariant in addition (i.e., addition of two elements preserves their ordering) and `β` is a preorder, if two functions `f` and `g` from `β` to `α` are strictly antitone on `s` (meaning that for any two distinct elements `a` and `b` in `s`, if `a` is less than `b`, then `f(b)` is less than `f(a)` and `g(b)` is less than `g(a)`), then the function defined as the sum of `f` and `g` is also strictly antitone on `s`. In other words, the sum of two functions that decrease when their inputs increase will also decrease when its input increases.
More concisely: If `f` and `g` are strictly antitone functions from a set `s` to an additive preorder `α` covariant in addition, then their sum is also a strictly antitone function on `s`.
|
Left.add_pos'
theorem Left.add_pos' :
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, 0 < a → 0 < b → 0 < a + b
This theorem, named `Left.add_pos'`, states that for any type `α` that has an addition operation with a zero element (i.e., it is an `AddZeroClass`), an order relation (i.e., it is a `Preorder`), and the addition operation is left covariant (i.e., it respects the order when we add an element to both sides), if `a` and `b` are elements of this type such that both are greater than zero, then their sum `a + b` is also greater than zero. The corresponding lemma that assumes right covariance instead is named `Right.add_pos'`.
More concisely: If `α` is an AddMonoid with zero element, Preorder, and left covariant addition, then for all `a b` in `α` with `0 < a` and `0 < b`, we have `0 < a + b`.
|
StrictMonoOn.add
theorem StrictMonoOn.add :
∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1],
StrictMonoOn f s → StrictMonoOn g s → StrictMonoOn (fun x => f x + g x) s
The theorem `StrictMonoOn.add` states that if we have two functions `f` and `g` that are strictly monotone on a set `s`, then the function that is the sum of `f` and `g` is also strictly monotone on `s`. Here, strict monotonicity means that for any two elements `a` and `b` in `s`, if `a` is less than `b`, then `f(a)` is less than `f(b)`. This property needs to hold in a context where `α` is a type supporting addition and both `α` and `β` are equipped with a preorder relation. Furthermore, `α` must be a covariant class under addition, meaning that addition preserves the preorder relation in `α`.
More concisely: If `f` and `g` are strictly monotone functions on a preordered set `s` where addition is covariant, then the function `f + g` is also strictly monotone on `s`.
|