PosSMulReflectLE.elim
theorem PosSMulReflectLE.elim :
∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α]
[self : PosSMulReflectLE α β] ⦃a : α⦄, 0 < a → ∀ ⦃b₁ b₂ : β⦄, a • b₁ ≤ a • b₂ → b₁ ≤ b₂
This theorem states that for any types `α` and `β` where `α` is a preordered smul type with zero and `β` is a preordered type, if there is a positive scalar multiplication reflectivity towards less than or equal relation between `α` and `β`, then for any positive `a` in `α`, if `a` times `b₁` is less than or equal to `a` times `b₂`, then `b₁` is also less than or equal to `b₂`. However, this theorem is deprecated and users are advised to use `le_of_smul_lt_smul_left` instead.
More concisely: If `α` is a preordered type with zero and `β` is a preordered type, and there is a positive scalar multiplication reflectivity from `α` to `β`, then for all positive `a` in `α` and `b₁, b₂` in `β`, if `a * b₁ ≤ a * b₂`, then `b₁ ≤ b₂`.
|
Mathlib.Algebra.Order.Module.Defs._auxLemma.18
theorem Mathlib.Algebra.Order.Module.Defs._auxLemma.18 :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, (0 ≤ -a) = (a ≤ 0)
This theorem, `Mathlib.Algebra.Order.Module.Defs._auxLemma.18`, states that for any type `α` that is an additive group and has a less-than-or-equal-to (`≤`) operation, and where the sum of two elements x and x_1 in that group is less than or equal to the sum of any other two elements in the group, then for any element `a` in that group, the statement that zero is less than or equal to the negation of `a` (`0 ≤ -a`) is equivalent to the statement that `a` is less than or equal to zero (`a ≤ 0`).
More concisely: For any additive group with a `≤` operation, if the sum of any two elements is less than or equal to the sum of any other two, then the negation of an element is less than or equal to zero if and only if that element is less than or equal to zero.
|
smul_add_smul_lt_smul_add_smul
theorem smul_add_smul_lt_smul_add_smul :
∀ {α : Type u_1} {β : Type u_2} [inst : OrderedRing α] [inst_1 : OrderedAddCommGroup β] [inst_2 : Module α β]
[inst_3 : PosSMulStrictMono α β] [inst_4 : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_5 : ContravariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {b₁ b₂ : α} {a d : β},
b₁ < b₂ → a < d → b₁ • d + b₂ • a < b₁ • a + b₂ • d
This theorem states the binary strict rearrangement inequality in the context of ordered rings and ordered additive commutative groups. Specifically, given two elements `b₁` and `b₂` from an ordered ring `α`, and two elements `a` and `d` from an ordered additive commutative group `β` that is also a module over `α`, if `b₁` is less than `b₂` and `a` is less than `d`, then the scalar multiplication of `b₁` and `d` plus the scalar multiplication of `b₂` and `a` is less than the scalar multiplication of `b₁` and `a` plus the scalar multiplication of `b₂` and `d`. This is essentially a statement about reordering terms in a certain way preserving an inequality under certain conditions.
More concisely: Given elements `b₁ < b₂` in an ordered ring `α` and `a < d` in an ordered additive commutative group `β` that is a module over `α`, we have `(b₁ : α) * d + (b₂ : α) * a < (b₁ : α) * a + (b₂ : α) * d`.
|
le_of_smul_le_smul_right
theorem le_of_smul_le_smul_right :
∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero β] [inst_4 : SMulPosReflectLE α β], a₁ • b ≤ a₂ • b → 0 < b → a₁ ≤ a₂
This theorem states that for any types `α` and `β`, and any elements `a₁`, `a₂` of `α` and `b` of `β`, given a scalar multiplication operation on `α` and `β`, and the preorder relations on `α` and `β`, if the scalar multiplication of `a₁` and `b` is less than or equal to the scalar multiplication of `a₂` and `b`, and if `b` is greater than zero, then `a₁` is less than or equal to `a₂`. The proof of this theorem is not provided (`sorry`). This theorem also requires `SMulPosReflectLE α β` which ensures that scalar multiplication reflects the preorder relation.
More concisely: If for types `α` and `β`, `a₁`, `a₂` in `α`, `b` in `β`, and a scalar multiplication `SMul` satisfying `SMulPosReflectLE α β`, we have `SMul a₁ b ≤ SMul a₂ b` and `b > 0`, then `a₁ ≤ a₂`.
|
le_inv_smul_iff_of_pos
theorem le_inv_smul_iff_of_pos :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : GroupWithZero α] [inst_1 : Preorder α]
[inst_2 : Preorder β] [inst_3 : MulAction α β] [inst_4 : PosSMulMono α β] [inst_5 : PosSMulReflectLE α β],
0 < a → (b₁ ≤ a⁻¹ • b₂ ↔ a • b₁ ≤ b₂)
This theorem states that for any two values `b₁` and `b₂` of some preordered type `β`, and any positive value `a` of a type `α` equipped with a group structure with zero and a multiplication action on `β`, the inequality `b₁ ≤ a⁻¹ • b₂` is equivalent to the inequality `a • b₁ ≤ b₂`. Here, `a⁻¹ • b₂` represents the scalar multiplication of `b₂` by the inverse of `a`, and `a • b₁` represents the scalar multiplication of `b₁` by `a`. This theorem assumes that scalar multiplication by positive elements of `α` is monotone and reflects the order of `β`.
More concisely: For any preordered type `β` with scalar multiplication by positive elements of a group `α` with zero, the inequality `b₁ ≤ a⁻¹ • b₂` is equivalent to `a • b₁ ≤ b₂`.
|
lt_of_smul_lt_smul_right
theorem lt_of_smul_lt_smul_right :
∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero β] [inst_4 : SMulPosReflectLT α β], a₁ • b < a₂ • b → 0 ≤ b → a₁ < a₂
This theorem, `lt_of_smul_lt_smul_right`, asserts that for any types `α` and `β`, given any two elements `a₁` and `a₂` of type `α` and an element `b` of type `β`, if type `α` can be scaled by type `β` (indicated by `SMul α β`) and both `α` and `β` are preordered (i.e., have a specified order property), if `b` is nonnegative, and if the multiplication of `α` and `β` reflects the order property (indicated by `SMulPosReflectLT α β`), then if `a₁ • b` is less than `a₂ • b`, it implies `a₁` is less than `a₂`. In other words, the theorem ensures that the order is maintained when scaling by a nonnegative factor.
More concisely: If `α` and `β` are preordered types with `α` scalable by `β` and `SMul PosReflectsLT` holds, then `a₁ < a₂` implies `a₁ * b < a₂ * b` for all nonnegative `b` in `β`.
|
lt_of_smul_lt_smul_of_nonneg
theorem lt_of_smul_lt_smul_of_nonneg :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero α] [inst_4 : PosSMulReflectLT α β], a • b₁ < a • b₂ → 0 ≤ a → b₁ < b₂
This theorem, `lt_of_smul_lt_smul_of_nonneg`, is an alias of `lt_of_smul_lt_smul_left`. It states that for any types `α` and `β`, along with elements `a` of `α` and `b₁`, `b₂` of `β`, under a scalar multiplication instance `SMul α β`, preorder structures on `α` and `β`, a zero instance on `α`, and posSMulReflectLT on `α` and `β`, if the scalar multiplication of `a` and `b₁` is less than the scalar multiplication of `a` and `b₂` and `a` is nonnegative, then `b₁` is less than `b₂`.
More concisely: If `a` is a non-negative element of `α`, `b₁` and `b₂` are elements of `β`, `SMul a b₁` is less than `SMul a b₂`, and `α` and `β` have preorders with `lt` and `zero`, then `b₁` is less than `b₂`.
|
smul_le_smul_iff_of_pos_left
theorem smul_le_smul_iff_of_pos_left :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero α] [inst_4 : PosSMulMono α β] [inst_5 : PosSMulReflectLE α β],
0 < a → (a • b₁ ≤ a • b₂ ↔ b₁ ≤ b₂)
This theorem states that for any types `α` and `β`, an action `SMul α β`, preorders on `α` and `β`, zero element in `α`, and given that multiplication by a positive number is monotone and reflects less than or equal to for `α` and `β`, if a positive number `a` is less than zero, then `a` multiplied by `b₁` is less than or equal to `a` multiplied by `b₂` if and only if `b₁` is less than or equal to `b₂`. This is a property related to the ordering of elements in a scalar multiplication context. The scalars are from an ordered field and the vectors are from an ordered vector space.
More concisely: For any ordered vector spaces α and β, and any positive number a in an ordered field, if b₁ ≤ b₂, then a * b₁ ≤ a * b₂.
|
lt_of_smul_lt_smul_left
theorem lt_of_smul_lt_smul_left :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero α] [inst_4 : PosSMulReflectLT α β], a • b₁ < a • b₂ → 0 ≤ a → b₁ < b₂
This theorem, `lt_of_smul_lt_smul_left`, states that for any types `α` and `β`, given elements `a` of type `α` and `b₁`, `b₂` of type `β`, and provided that `α` and `β` are preordered, `α` has a zero element, and the operation of scalar multiplication reflects the "less than" relation, if `a` times `b₁` is less than `a` times `b₂` and `a` is non-negative, then `b₁` is less than `b₂`. In other words, in the given conditions, if scaling `b₁` by `a` results in a value less than scaling `b₂` by `a`, then `b₁` must be less than `b₂`.
More concisely: If `α` is a preordered type with a zero element and scalar multiplication is order-preserving, then for all `a ∈ α` non-negative and `b₁, b₂ ∈ β`, if `a * b₁` < `a * b₂`, then `b₁` < `b₂`.
|
le_inv_smul_iff
theorem le_inv_smul_iff :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : GroupWithZero α] [inst_1 : Preorder α]
[inst_2 : Preorder β] [inst_3 : MulAction α β] [inst_4 : PosSMulMono α β] [inst_5 : PosSMulReflectLE α β],
0 < a → (b₁ ≤ a⁻¹ • b₂ ↔ a • b₁ ≤ b₂)
This theorem, `le_inv_smul_iff`, establishes a rule for positive scalar multiplication in the context of a group with zero and preorders. Given two types `α` and `β`, where `α` is a group with zero and both `α` and `β` have preorder relationships, if `a` is a positive element in `α`, and `b₁` and `b₂` are elements in `β`, then `b₁` is less than or equal to the inverse of `a` scaled by `b₂` if and only if `a` scaled by `b₁` is less than or equal to `b₂`. This theorem is particularly useful in fields like analysis and linear algebra, where scalar multiplication often interacts with order relationships.
More concisely: Given a group with zero `α` and a preordered type `β`, for all positive `a` in `α` and `b₁, b₂` in `β`, `b₁ ≤ b₂` if and only if `a * b₁ ≤ a * b₂`.
|
SMulPosReflectLE.elim
theorem SMulPosReflectLE.elim :
∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero β]
[self : SMulPosReflectLE α β] ⦃b : β⦄, 0 < b → ∀ ⦃a₁ a₂ : α⦄, a₁ • b ≤ a₂ • b → a₁ ≤ a₂
This theorem, titled `SMulPosReflectLE.elim`, states that for any types `α` and `β`, where `α` has a scalar multiplication operation with `β`, and both `α` and `β` have a preorder relation, and `β` has a zero element, and there's a positive reflection property for scalar multiplication and preorder on `α` and `β`. Given a positive `b` of type `β`, for any elements `a₁` and `a₂` of type `α`, if `a₁` scalar multiplied with `b` is less than or equal to `a₂` scalar multiplied with `b`, then `a₁` is less than or equal to `a₂`. However, this theorem is deprecated and `le_of_smul_lt_smul_right` is recommended for use instead.
More concisely: If for types `α` and `β`, `α` has a scalar multiplication operation with `β`, `β` has a zero element, `α` and `β` have preorders with positive reflection property for scalar multiplication, and `b` is a positive element of `β`, then `a₁ ≤ a₂` implies `a₁ * b ≤ a₂ * b` for all `a₁, a₂` in `α`.
|
smul_pos_of_neg_of_neg
theorem smul_pos_of_neg_of_neg :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : OrderedRing α] [inst_1 : OrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : PosSMulStrictMono α β] [inst_4 : PosSMulReflectLT α β],
a < 0 → b < 0 → 0 < a • b
This theorem, "smul_pos_of_neg_of_neg", states that for any two types `α` and `β` with `α` being an ordered ring and `β` being an ordered additive commutative group, and given a module structure on `α` and `β` and two properties: strictly monotonically increasing scalar multiplication (`PosSMulStrictMono`) and reflection of inequality under positive scalar multiplication (`PosSMulReflectLT`), if `a` is a negative element of `α` and `b` is a negative element of `β`, then the scalar product of `a` and `b` is positive. The scalar product is defined as `a` times `b`, denoted as `a • b`.
More concisely: For any ordered ring `α` and ordered additive commutative group `β` with strictly monotonically increasing scalar multiplication and reflection of inequality under positive scalar multiplication, the product of a negative element in `α` and a negative element in `β` is positive.
|
smul_le_smul_of_nonneg_right
theorem smul_le_smul_of_nonneg_right :
∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero β] [inst_4 : SMulPosMono α β], a₁ ≤ a₂ → 0 ≤ b → a₁ • b ≤ a₂ • b
This theorem states that for any types `α` and `β`, along with any two elements `a₁` and `a₂` of type `α` and an element `b` of type `β`, given that there is a scalar multiplication operation defined on `α` and `β`, and assuming `α` and `β` are both preordered (i.e., they have a less than or equal to relation defined that is reflexive and transitive), and `β` has a zero element, and the scalar multiplication is positive monotonic (meaning that if `a₁` is less than or equal to `a₂`, then `a₁` multiplied by any positive `b` is less than or equal to `a₂` multiplied by `b`), then if `a₁` is less than or equal to `a₂` and `b` is non-negative, `a₁ • b` is less than or equal to `a₂ • b`.
More concisely: If `α` and `β` are preordered types with zero elements and scalar multiplication is positive monotonic, then for any `a₁ ≤ a₂` in `α` and non-negative `b` in `β`, `a₁ • b ≤ a₂ • b`.
|
smul_le_smul_iff_of_neg_left
theorem smul_le_smul_iff_of_neg_left :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : OrderedRing α] [inst_1 : OrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : PosSMulMono α β] [inst_4 : PosSMulReflectLE α β],
a < 0 → (a • b₁ ≤ a • b₂ ↔ b₂ ≤ b₁)
The theorem `smul_le_smul_iff_of_neg_left` states that for any types `α` and `β`, with `α` being an ordered ring, `β` being an ordered additive commutative group, and `α` also being a module over `β`, if `a` is a negative element of `α` and `b₁` and `b₂` are arbitrary elements of `β`, then scalar multiplication of `a` and `b₁` is less than or equal to scalar multiplication of `a` and `b₂` if and only if `b₂` is less than or equal to `b₁`. This theorem thus provides a way to compare scalar multiples under the conditions that the scalar is negative and the module operation and scalar multiplication obey certain properties (`PosSMulMono` and `PosSMulReflectLE`).
More concisely: For any ordered ring `α`, ordered additive commutative group `β`, and `α` being a module over `β`, if `a` is negative in `α` and `b₁ ≤ b₂` in `β`, then `-(a * b₁) ≤ (a * b₂)` in `α`.
|
smul_neg_iff_of_pos
theorem smul_neg_iff_of_pos :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β]
[inst_3 : Preorder α] [inst_4 : Preorder β] [inst_5 : PosSMulStrictMono α β] [inst_6 : PosSMulReflectLT α β],
0 < a → (a • b < 0 ↔ b < 0)
This theorem, `smul_neg_iff_of_pos`, states that for any types `α` and `β` where `α` is a scalar and `β` is a vector such that `α` has a zero element, `β` has a zero element, and scalar multiplication on `α` and `β` behaves in a certain way (`SMulZeroClass`), and both `α` and `β` have an order relation (`Preorder`), we have the following property. If multiplication by a positive scalar strictly increases the value in the order (`PosSMulStrictMono`), and reflects the inequality when multiplying by a positive scalar (`PosSMulReflectLT`), then if `a` is positive, the inequality `a • b < 0` is true if and only if `b < 0`. Here, `a • b` denotes scalar multiplication of `b` by `a`.
More concisely: For types `α` and `β` with scalar multiplication `•` satisfying `SMulZeroClass`, `Preorder`, `PosSMulStrictMono`, and `PosSMulReflectLT`, if `a` is positive in `α`, then `a • b < 0` if and only if `b` is negative in `β`.
|
smul_le_smul_of_nonneg_left
theorem smul_le_smul_of_nonneg_left :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero α] [inst_4 : PosSMulMono α β], b₁ ≤ b₂ → 0 ≤ a → a • b₁ ≤ a • b₂
This theorem, `smul_le_smul_of_nonneg_left`, states that for any types `α` and `β`, and for any elements `a` of `α` and `b₁` and `b₂` of `β`, given that `α` and `β` have a multiplication (`SMul α β`), that `α` and `β` are preordered (meaning that they have a "less than or equal to" relation), and that `α` has a zero and a positive, strictly monotonic multiplication with `β`; if `b₁` is less than or equal to `b₂` and `a` is nonnegative (greater than or equal to zero), then the product of `a` and `b₁` is less than or equal to the product of `a` and `b₂`. This is a generalization of the property of real numbers that if `x ≤ y` and `0 ≤ a`, then `a*x ≤ a*y`.
More concisely: For any types `α` and `β` with multiplication, preorder, zero, and positive element, if `a ≥ 0`, `b₁ ≤ b₂`, then `a * b₁ ≤ a * b₂`.
|
lt_inv_smul_iff
theorem lt_inv_smul_iff :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : GroupWithZero α] [inst_1 : Preorder α]
[inst_2 : Preorder β] [inst_3 : MulAction α β] [inst_4 : PosSMulStrictMono α β] [inst_5 : PosSMulReflectLT α β],
0 < a → (b₁ < a⁻¹ • b₂ ↔ a • b₁ < b₂)
This theorem, `lt_inv_smul_iff`, is an alias of `lt_inv_smul_iff_of_pos`. It's a mathematical statement that exists within the context of a group with zero and two pre-ordered sets. Specifically, it states that for any positive `a` from the group, and `b₁`, `b₂` from the preordered sets, the inequality `b₁ < a⁻¹ • b₂` is equivalent to `a • b₁ < b₂`. Here `•` denotes a multiplication action of the group on the preordered set, `a⁻¹` denotes the multiplicative inverse of `a`, and `<` denotes the ordering on the preordered set.
More concisely: For any positive group element `a` and preordered set elements `b₁, b₂`, the inequality `a • b₁ < b₂` is equivalent to `b₁ < a⁻¹ • b₂`.
|
smul_pos_iff_of_neg
theorem smul_pos_iff_of_neg :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : OrderedRing α] [inst_1 : OrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : PosSMulStrictMono α β] [inst_4 : PosSMulReflectLT α β],
a < 0 → (0 < a • b ↔ b < 0)
This theorem, `smul_pos_iff_of_neg`, is an alias of `smul_pos_iff_of_neg_left`. It states that for any ordered ring `α`, ordered add commutative group `β`, elements `a` from `α` and `b` from `β`, along with the conditions that `α` is a module over `β`, and `α` and `β` satisfy positive scalar multiplication strict monotonicity and positive scalar multiplication reflects less than, if `a` is less than zero, then `a` scalar multiplied by `b` is positive if and only if `b` is less than zero.
More concisely: For an ordered ring `α` and an ordered add commutative group `β` with positive scalar multiplication strict monotonicity and reflecting less than, if `a` is negative in `α` and `b` is positive in `β`, then `a * b` is positive in `α`.
|
smul_nonneg
theorem smul_nonneg :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β]
[inst_3 : Preorder α] [inst_4 : Preorder β] [inst_5 : PosSMulMono α β], 0 ≤ a → 0 ≤ b₁ → 0 ≤ a • b₁
This theorem, `smul_nonneg`, states that for any types `α` and `β`, and for any elements `a` of type `α` and `b₁` of type `β`, given that `α` and `β` have zero elements, `α` and `β` form a scalar multiplication zero class, and both `α` and `β` are preordered (that is, they are equipped with an associative, transitive and reflexive relation), and positive scalar multiplication is monotonic on `α` and `β`, then if `a` and `b₁` are both nonnegative (i.e., `0 ≤ a` and `0 ≤ b₁`), the scalar multiplication of `a` and `b₁` (denoted as `a • b₁`) is also nonnegative (i.e., `0 ≤ a • b₁`).
More concisely: If `α` and `β` are preordered types with zero elements and scalar multiplication is monotonic and defines a zero class, then for all nonnegative `a` in `α` and `b₁` in `β`, `a • b₁` is nonnegative.
|
smul_lt_smul_iff_of_neg
theorem smul_lt_smul_iff_of_neg :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : OrderedRing α] [inst_1 : OrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : PosSMulStrictMono α β] [inst_4 : PosSMulReflectLT α β],
a < 0 → (a • b₁ < a • b₂ ↔ b₂ < b₁)
This theorem, `smul_lt_smul_iff_of_neg`, is an alias of `smul_lt_smul_iff_of_neg_left`. It states that for any types `α` and `β`, with `α` being an ordered ring and `β` being an ordered additive commutative group, and for any elements `a` of `α` and `b₁, b₂` of `β`, given that also `β` is a module over `α`, and assuming an instance of positive scalar multiplication being strictly monotone and another instance of positive scalar multiplication reflecting less than, if `a` is less than zero, then `a` scalar multiplied by `b₁` is less than `a` scalar multiplied by `b₂` if and only if `b₂` is less than `b₁`. This theorem basically describes the relationship between scalar multiplication and ordering in the context of negative scalars.
More concisely: Given an ordered ring `α` and an ordered additive commutative group `β` with positive scalar multiplication being strictly monotone and reflecting less than, for all `a < 0` in `α` and `b₁, b₂` in `β`, `a * b₁ < a * b₂` if and only if `b₂ < b₁`.
|
smul_lt_smul_iff_of_pos_right
theorem smul_lt_smul_iff_of_pos_right :
∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero β] [inst_4 : SMulPosStrictMono α β] [inst_5 : SMulPosReflectLT α β],
0 < b → (a₁ • b < a₂ • b ↔ a₁ < a₂)
This theorem states that for any two elements `a₁` and `a₂` of a partially ordered type `α`, and any element `b` of a partially ordered type `β`, given the conditions that `β` has a zero element, `α` and `β` have a scalar multiplication operation, and this scalar multiplication operation is strictly monotonically increasing and reflects the less than operator when multiplied by a positive element, then if `b` is positive, `a₁` is less than `a₂` if and only if the result of scalar multiplication of `a₁` and `b` is less than the result of scalar multiplication of `a₂` and `b`. In mathematical terms, if `0 < b`, then `a₁ • b < a₂ • b` is equivalent to `a₁ < a₂`.
More concisely: For any partially ordered types `α` and `β` with a zero element and a strictly monotonically increasing scalar multiplication operation, if `β` has a positive element `b`, then `a₁ < a₂` if and only if `a₁ · b < a₂ · b` for all `a₁, a₂ ∈ α`.
|
strict_mono_smul_left
theorem strict_mono_smul_left :
∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero α] [inst_4 : PosSMulStrictMono α β], 0 < a → StrictMono fun x => a • x
The theorem `strict_mono_smul_left` states that for any types `α` and `β`, given that `α` is a scalar multiplication (`SMul`) on `β`, `α` and `β` are preorders, `α` has a zero element, and positive scalar multiplication is strictly monotonic (`PosSMulStrictMono`) on `α` and `β`, then if a scalar `a` of type `α` is greater than zero, the function that maps an element `x` to `a * x` (scalar multiplication of `a` and `x`) is strictly monotonic. Explicitly, for any pair of elements such that the first is less than the second, the result of multiplying `a` by the first element is less than the result of multiplying `a` by the second.
More concisely: Given a type `β` with a preorder structure, and a scalar multiplication `α` on `β` with a positive zero element and strictly monotonic positive scalar multiplication, the function `x mapsto a * x` is strictly monotonic for any positive scalar `a` in `α`.
|
Mathlib.Algebra.Order.Module.Defs._auxLemma.17
theorem Mathlib.Algebra.Order.Module.Defs._auxLemma.17 :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α}, (0 < -a) = (a < 0)
This theorem, named `Mathlib.Algebra.Order.Module.Defs._auxLemma.17`, states that for all types `α` that are instances of an `AddGroup` and have a `Less Than (LT)` operation, and for which the addition operation `x + x_1` is covariant with the less than operation `x < x_1`, the statement "0 is less than the negation of `a`" is equivalent to the statement "`a` is less than 0". Here, `a` is an arbitrary element of the type `α`. This theorem connects the concepts of negation, addition, and order in the context of a mathematical structure like a group.
More concisely: For an additive group type `α` with a covariant addition and a `LT` order relation, `0 < -a` if and only if `a < 0`.
|
smul_lt_smul_of_pos_left
theorem smul_lt_smul_of_pos_left :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero α] [inst_4 : PosSMulStrictMono α β], b₁ < b₂ → 0 < a → a • b₁ < a • b₂
This theorem states that for any types `α` and `β`, given scalar multiplication (`SMul`) on `α` and `β`, an ordering on `α` (`Preorder α`), an ordering on `β` (`Preorder β`), a zero element on `α` (`Zero α`), and a positive strict monotonicity of scalar multiplication (`PosSMulStrictMono α β`), if `b₁` is less than `b₂` and `a` is greater than zero, then the scalar multiplication of `a` and `b₁` is less than the scalar multiplication of `a` and `b₂`. In mathematical notation, it asserts that if `b₁ < b₂` and `0 < a`, then `a * b₁ < a * b₂`. This theorem formalizes a property of order-preserving scalar multiplication.
More concisely: For types `α` and `β` with orderings, zero elements, and positive strict monotonic scalar multiplications, if `0 < a` and `b₁ < b₂`, then `a * b₁ < a * b₂`.
|
PosSMulMono.of_pos
theorem PosSMulMono.of_pos :
∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
[inst_3 : PartialOrder α] [inst_4 : Preorder β],
(∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂) → PosSMulMono α β
The Lean theorem `PosSMulMono.of_pos` provides a constructor for `PosSMulMono` (Positive Scalar Multiplication is Monotone) under some conditions on the types α and β and their operations. The theorem states that for all α and β, if α is greater than zero, then if β1 is less than or equal to β2, the scalar multiplication of α and β1 is also less than or equal to the scalar multiplication of α and β2. This theorem is valid under the conditions that α and β are types with zero elements, α and β have scalar multiplication with zero, α has a partial order, and β has a preorder.
More concisely: For types α with a partial order and β with a preorder having scalar multiplication, if α is positive and β1 ≤ β2, then α * β1 ≤ α * β2.
|
PosSMulMono.elim
theorem PosSMulMono.elim :
∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α]
[self : PosSMulMono α β] ⦃a : α⦄, 0 ≤ a → ∀ ⦃b₁ b₂ : β⦄, b₁ ≤ b₂ → a • b₁ ≤ a • b₂
This theorem, which is not recommended for use (favor `smul_le_smul_of_nonneg_left` instead), states that in a context where we have two types `α` and `β` with a scalar multiplication operation, and `α` and `β` both have a preorder (reflexive and transitive binary relation), and `α` has a zero, and the scalar multiplication by a positive element is monotonous, then for any nonnegative scalar `a`, if one element `b₁` is less than or equal to another element `b₂`, then the result of scalar multiplication of `a` and `b₁` is less than or equal to the result of scalar multiplication of `a` and `b₂`. This is essentially saying that scalar multiplication preserves the order.
More concisely: If `α` and `β` are types with a preorder and scalar multiplication, `α` has a zero, and scalar multiplication by positive scalars is monotone, then for all nonnegative scalars `a` and `α` elements `b₁ ≤ b₂`, we have `a * b₁ ≤ a * b₂`.
|
SMulPosMono.of_pos
theorem SMulPosMono.of_pos :
∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] [inst_3 : Preorder α]
[inst_4 : PartialOrder β], (∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b) → SMulPosMono α β
This theorem, `SMulPosMono.of_pos`, provides a constructor for the `SMulPosMono` structure. It works for any types `α` and `β` where `α` has a zero element and an ordering, `β` has a zero element and a partial ordering, and scalar multiplication with zero is defined for `α` and `β`. The constructor requires a proof that for all `b` in `β`, if `0 < b`, then for any `a₁` and `a₂` in `α` such that `a₁ ≤ a₂`, it must be the case that `a₁ • b ≤ a₂ • b`. In other words, it requires a proof that scalar multiplication is monotonically increasing for positive `b`.
More concisely: For types `α` with a zero element and ordering, and `β` with a zero element and partial ordering, if scalar multiplication with positive elements of `β` is monotonically increasing on `α`, then `α × β` has the `SMulPosMono` structure.
|
SMulPosMono.elim
theorem SMulPosMono.elim :
∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero β]
[self : SMulPosMono α β] ⦃b : β⦄, 0 ≤ b → ∀ ⦃a₁ a₂ : α⦄, a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
This theorem, which you should not use and instead use `smul_le_smul_of_nonneg_right`, states that for any types `α` and `β` with a scalar multiplication (`SMul α β`), a preorder on `α` and `β` (which is a reflexive and transitive binary relation), and a zero element in `β` (`Zero β`); and for any scalar multiplication that preserves positivity (`SMulPosMono α β`), if `b` is a nonnegative member of type `β`, then for any members `a₁` and `a₂` of type `α`, if `a₁` is less than or equal to `a₂`, then the scalar multiplication of `a₁` and `b` is less than or equal to the scalar multiplication of `a₂` and `b`. In simpler terms, it states that scalar multiplication by a nonnegative number preserves order.
More concisely: For any types with scalar multiplication, if `a₁ ≤ a₂` in `α` and `b` is nonnegative in `β`, then `a₁ * b ≤ a₂ * b`.
|
smul_lt_smul_iff_of_neg_left
theorem smul_lt_smul_iff_of_neg_left :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : OrderedRing α] [inst_1 : OrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : PosSMulStrictMono α β] [inst_4 : PosSMulReflectLT α β],
a < 0 → (a • b₁ < a • b₂ ↔ b₂ < b₁)
The theorem `smul_lt_smul_iff_of_neg_left` states that for any type `α` forming an ordered ring, a second type `β` forming an ordered additive commutative group, and elements `a` of type `α` and `b₁`, `b₂` of type `β`, given that the type `β` is a module over `α` and that the scalar multiplication operation is strictly monotonically increasing and reflects less-than relations when the scalar is positive, if `a` is less than zero, then scalar multiplication of `a` and `b₁` being less than scalar multiplication of `a` and `b₂` is equivalent to `b₂` being less than `b₁`. This means that when the scaling factor is negative, the order of elements changes when scaled.
More concisely: For any ordered ring `α`, ordered additive commutative group `β` making `β` a `α`-module, and `a ∈ α`, `b₁, b₂ ∈ β`, if `a < 0` then `a * b₁ < a * b₂` if and only if `b₂ < b₁`.
|
inv_smul_le_iff
theorem inv_smul_le_iff :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : GroupWithZero α] [inst_1 : Preorder α]
[inst_2 : Preorder β] [inst_3 : MulAction α β] [inst_4 : PosSMulMono α β] [inst_5 : PosSMulReflectLE α β],
0 < a → (a⁻¹ • b₁ ≤ b₂ ↔ b₁ ≤ a • b₂)
The theorem `inv_smul_le_iff` is a general rule about order and scalar multiplication in the context of groups and preorders. Specifically, for any types `α` and `β`, a scalar `a` in `α`, and elements `b₁` and `b₂` in `β` (where `α` is a group with zero, `β` is a preorder, and scalar multiplication on `β` is compliant with `α`'s order), if `a` is positive, then the inequality `a⁻¹ • b₁ ≤ b₂` is equivalent to `b₁ ≤ a • b₂`. This theorem serves as an alias for `inv_smul_le_iff_of_pos`.
More concisely: For any group `α` with zero, preorder `β`, and compliant scalar multiplication, if `a` is a positive element of `α` then `a⁻¹ • b₁ ≤ b₂` is equivalent to `b₁ ≤ a • b₂`.
|
SMulPosStrictMono.elim
theorem SMulPosStrictMono.elim :
∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero β]
[self : SMulPosStrictMono α β] ⦃b : β⦄, 0 < b → ∀ ⦃a₁ a₂ : α⦄, a₁ < a₂ → a₁ • b < a₂ • b
This theorem states that for any types `α` and `β`, given an implementation of scalar multiplication (`SMul α β`), a preorder relationship on `α` and `β`, and zero defined for `β`, and provided `SMulPosStrictMono α β` holds, if `b` is a positive number of type `β`, then for any `a₁` and `a₂` of type `α` such that `a₁` is less than `a₂`, scalar multiplication of `a₁` and `b` is lesser than scalar multiplication of `a₂` and `b`. However, this theorem should not be used directly. Instead, `smul_lt_smul_of_pos_right` should be used.
More concisely: For any types `α` and `β` with a preorder, zero, and scalar multiplication defined, if `SMulPosStrictMono α β` holds and `b` is positive in `β`, then for all `a₁ ≤ a₂` in `α`, `SMul a₁ b < SMul a₂ b`.
|
smul_neg_iff_of_neg
theorem smul_neg_iff_of_neg :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : OrderedRing α] [inst_1 : OrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : PosSMulStrictMono α β] [inst_4 : PosSMulReflectLT α β],
a < 0 → (a • b < 0 ↔ 0 < b)
This theorem, `smul_neg_iff_of_neg`, states that for any ordered ring `α`, any ordered additive commutative group `β`, any instances `a` in `α`, `b` in `β`, and assuming `α` and `β` form a module and have properties of positive strict multiplication monotonicity and positive scalar multiplication reflection less than, if `a` is less than 0, then the scalar multiplication of `a` and `b` is less than 0 if and only if `b` is greater than 0.
More concisely: For any ordered ring `α` and ordered additive commutative group `β` forming a module, if `a` is a negative element in `α` and `b` is a positive element in `β`, then `a * b` is a negative number.
|
SMulPosReflectLT.elim
theorem SMulPosReflectLT.elim :
∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero β]
[self : SMulPosReflectLT α β] ⦃b : β⦄, 0 ≤ b → ∀ ⦃a₁ a₂ : α⦄, a₁ • b < a₂ • b → a₁ < a₂
This theorem, which is not recommended for use and prefer to use 'lt_of_smul_lt_smul_right' instead, states that for all types α and β where α has a scalar multiplication with β and both α and β have a preorder relation, and β has a zero element, given an element b of β which is greater than or equal to zero, for any two elements a₁ and a₂ of α, if scalar multiplication of a₁ and b is less than scalar multiplication of a₂ and b, then a₁ is less than a₂. This theorem is related to the 'SMulPosReflectLT' typeclass, which reflects the comparison of positive numbers under scalar multiplication.
More concisely: For types α and β with scalar multiplication and preorder relations, and β having a zero element, if b is a non-negative element of β and a₁ scalar multiplied by b is less than a₂ scalar multiplied by b, then a₁ is less than a₂ in α.
|
SMulPosReflectLT.of_pos
theorem SMulPosReflectLT.of_pos :
∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] [inst_3 : Preorder α]
[inst_4 : PartialOrder β], (∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂) → SMulPosReflectLT α β
The theorem `SMulPosReflectLT.of_pos` provides a constructor for `SMulPosReflectLT` type in Lean 4. According to it, for any two types `α` and `β` with the conditions that `α` has a zero element, `β` has a zero element, `α` and `β` have a scalar multiplication operation with zero, `α` has a preorder relation, and `β` has a partial order relation, if for all `b` in `β`, whenever `b` is greater than zero and for any `a₁` and `a₂` in `α`, if `a₁` scaled by `b` is less than `a₂` scaled by `b`, then `a₁` is less than `a₂`, then `α` and `β` have the property `SMulPosReflectLT`. This expresses that the ordering in `α` can be induced by scalar multiplication with positive elements in `β`.
More concisely: Given types `α` and `β` with zero elements, scalar multiplication, and preorder/partial order relations such that multiplication by any positive element in `β` preserves the ordering in `α`, then `α` and `β` have the property of `SMulPosReflectLT`.
|
smul_add_smul_le_smul_add_smul'
theorem smul_add_smul_le_smul_add_smul' :
∀ {α : Type u_1} {β : Type u_2} [inst : OrderedRing α] [inst_1 : OrderedAddCommGroup β] [inst_2 : Module α β]
[inst_3 : PosSMulMono α β] [inst_4 : ContravariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{b₁ b₂ : α} {a d : β}, b₂ ≤ b₁ → d ≤ a → b₁ • d + b₂ • a ≤ b₁ • a + b₂ • d
The theorem `smul_add_smul_le_smul_add_smul'` states the binary rearrangement inequality in the context of ordered rings and ordered additive commutative groups. More specifically, for any types `α` and `β`, where `α` is an ordered ring, `β` is an ordered additive commutative group and `β` is a module over `α`, the theorem states that if `b₂` is less than or equal to `b₁`, and `d` is less than or equal to `a`, then the scalar multiplication of `b₁` and `d` added to the scalar multiplication of `b₂` and `a` is less than or equal to the scalar multiplication of `b₁` and `a` added to the scalar multiplication of `b₂` and `d`.
More concisely: For any ordered ring `α`, ordered additive commutative group `β` (as an `α`-module), `b₂ ≤ b₁`, and `d ≤ a`, we have `(b₁ : β) * d + (b₂ : β) * a ≤ (b₁ : β) * a + (b₂ : β) * d`.
|
smul_lt_smul_of_neg
theorem smul_lt_smul_of_neg :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : OrderedRing α] [inst_1 : OrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : PosSMulStrictMono α β], b₁ < b₂ → a < 0 → a • b₂ < a • b₁
This theorem, called `smul_lt_smul_of_neg`, states that for any two types `α` and `β`, any member `a` of `α`, and any two members `b₁` and `b₂` of `β`, given that `α` is an ordered ring, `β` is an ordered additive commutative group, and `β` is a module over `α` with strictly monotonic positive scalar multiplication, if `b₁` is less than `b₂` and `a` is less than zero, then `a` scaled by `b₂` is less than `a` scaled by `b₁`. In mathematical terms, if $b₁ < b₂$ and $a < 0$, then $a \cdot b₂ < a \cdot b₁$.
More concisely: For any ordered ring `α`, ordered additive commutative group and `β`-module `β` with strictly monotonic positive scalar multiplication, if `a` is a negative element of `α` and `b₁` is strictly less than `b₂` in `β`, then `a` multiplied by `b₂` is strictly less than `a` multiplied by `b₁`.
|
inv_smul_lt_iff
theorem inv_smul_lt_iff :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : GroupWithZero α] [inst_1 : Preorder α]
[inst_2 : Preorder β] [inst_3 : MulAction α β] [inst_4 : PosSMulStrictMono α β] [inst_5 : PosSMulReflectLT α β],
0 < a → (a⁻¹ • b₁ < b₂ ↔ b₁ < a • b₂)
The theorem `inv_smul_lt_iff` states that for a given type `α` with a GroupWithZero structure and a type `β` with a Preorder structure that also has a MulAction, a PosSMulStrictMono, and a PosSMulReflectLT structure over `α`, for all `a` of type `α` and `b₁`, `b₂` of type `β`, if `a` is greater than zero then the inequality `a⁻¹ • b₁ < b₂` holds if and only if `b₁ < a • b₂`. Here, `•` denotes the scalar multiplication action of `α` on `β`, and `a⁻¹` denotes the multiplicative inverse of `a` in the group with zero `α`.
More concisely: For any type `α` with a GroupWithZero structure and a Preorder `β` with MulAction, PosSMulStrictMono, and PosSMulReflectLT structures over `α`, the multiplicative inverse `a^{-1}` of a positive element `a` in `α` satisfies `a^{-1} • b₁ < b₂` if and only if `b₁ < a • b₂`, where `•` denotes the scalar multiplication action.
|
monotone_smul_left_of_nonneg
theorem monotone_smul_left_of_nonneg :
∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero α] [inst_4 : PosSMulMono α β], 0 ≤ a → Monotone fun x => a • x
The theorem `monotone_smul_left_of_nonneg` states that for any types `α` and `β`, given an element `a` of type `α`, and given that `α` and `β` are preordered, `α` has a zero, and `α` and `β` have a positively monotone scalar multiplication operation, if `a` is non-negative (i.e., `0 ≤ a`), then the function that maps `x` to the scalar multiplication of `a` and `x` (i.e., `a • x`) is monotone. In other words, if `a` is non-negative, increasing `x` will not decrease `a • x`.
More concisely: If `α` is a preordered type with a zero, `β` is another type, `a : α` is non-negative, and `α` and `β` have a positively monotone scalar multiplication, then the function `x => a • x` is monotone on `α`.
|
strict_anti_smul_left
theorem strict_anti_smul_left :
∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : OrderedRing α] [inst_1 : OrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : PosSMulStrictMono α β], a < 0 → StrictAnti fun x => a • x
The theorem `strict_anti_smul_left` states that for any types `α` and `β`, where `α` is an ordered ring and `β` is an ordered additive commutative group that also has a module structure over `α` and is strictly monotonically increasing under positive scalar multiplication, if a given element `a` of `α` is less than zero, then the function defined as scalar multiplication by `a` is strictly antitone. In other words, if `a` is negative, then multiplying any element `x` of `β` by `a` reverses the order of the elements.
More concisely: For any ordered ring `α` and strictly monotonically increasing `α`-module `β` over a negative element `a` in `α`, scalar multiplication by `a` reverses the order.
|
smul_lt_smul_of_pos_right
theorem smul_lt_smul_of_pos_right :
∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero β] [inst_4 : SMulPosStrictMono α β], a₁ < a₂ → 0 < b → a₁ • b < a₂ • b
This theorem, named `smul_lt_smul_of_pos_right`, states that for any types `α` and `β`, given two elements `a₁` and `a₂` of type `α`, and an element `b` of type `β`, under the conditions that `α` is equipped with a scalar multiplication operation (`SMul α β`), `α` and `β` are both preordered (`Preorder α` and `Preorder β`), `β` has a zero (`Zero β`), and the scalar multiplication operation is strictly monotonically increasing when `b` is positive (`SMulPosStrictMono α β`), if `a₁` is less than `a₂` and `b` is greater than zero, then the result of scalar multiplication of `a₁` and `b` is less than the result of scalar multiplication of `a₂` and `b`. In mathematical notation, this can be written as: if $a_1 < a_2$ and $b > 0$, then $a_1 \cdot b < a_2 \cdot b$.
More concisely: Given types `α` and `β` with scalar multiplication `SMul α β`, `Preorder α`, `Preorder β`, `Zero β`, and `SMulPosStrictMono α β`, if `a₁ < a₂` in `α` and `b > 0` in `β`, then `a₁ * b < a₂ * b`.
|
smul_max
theorem smul_max :
∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : LinearOrder β]
[inst_3 : Zero α] [inst_4 : PosSMulMono α β], 0 ≤ a → ∀ (b₁ b₂ : β), a • max b₁ b₂ = max (a • b₁) (a • b₂)
This theorem, "smul_max", is an alias of `smul_max_of_nonneg`. It asserts that for any types `α` and `β`, given an element `a` of type `α`, and `b₁` and `b₂` of type `β`, if `α` is a preordered semimodule over `β`, `β` has a linear order, `α` has a zero element, and positive scalar multiplication is monotone for `α` and `β`, then if `a` is nonnegative (`0 ≤ a`), scalar multiplication of `a` with the maximum of `b₁` and `b₂` (`a • max b₁ b₂`) equals the maximum of the scalar multiplication of `a` with `b₁` and `b₂` (`max (a • b₁) (a • b₂)`). This essentially states that scalar multiplication distributes over the maximum operation for nonnegative scalars.
More concisely: If `α` is a preordered semimodule over a linearly ordered type `β` with a zero element, and positive scalar multiplication is monotone for both `α` and `β`, then for any nonnegative `a` in `α`, we have `a • max b₁ b₂ = max (a • b₁) (a • b₂)`.
|
antitone_smul_left
theorem antitone_smul_left :
∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : OrderedRing α] [inst_1 : OrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : PosSMulMono α β], a ≤ 0 → Antitone fun x => a • x
The theorem `antitone_smul_left` states that for any ordered ring `α`, ordered additive commutative group `β`, module `α β`, and positive scalar multiplication monotonic structure `PosSMulMono α β`, if a given element `a` of `α` is less than or equal to zero, then scalar multiplication by `a` is an antitone (or decreasing) function. In other words, if `a ≤ b`, then `a • x ≤ b • x` for all `x` in `β`.
More concisely: For any ordered ring `α`, ordered additive commutative group `β`, module `α β`, and positive scalar multiplication monotonic structure `PosSMulMono α β`, if `a ≤ 0` in `α`, then for all `x` in `β`, `a • x ≤ 0 • x` or equivalently, `a • x ≤ b • x` for all `b ≥ a` in `α`.
|
lt_of_smul_lt_smul_of_nonneg_right
theorem lt_of_smul_lt_smul_of_nonneg_right :
∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero β] [inst_4 : SMulPosReflectLT α β], a₁ • b < a₂ • b → 0 ≤ b → a₁ < a₂
This theorem, an alias of `lt_of_smul_lt_smul_right`, states that for any types `α` and `β`, given `a₁`, `a₂` of type `α`, `b` of type `β`, and assuming that `α` and `β` are both preordered, `β` has a zero, and scalar multiplication of `α` on `β` reflects positivity to less-than ordering, if the scalar multiplication of `a₁` and `b` is less than the scalar multiplication of `a₂` and `b`, and `b` is non-negative, then `a₁` is less than `a₂`.
More concisely: If `α` and `β` are preordered types with `β` having a zero and `α`'s scalar multiplication on `β` preserves less-than ordering, then for all `a₁ ≤ a₂` in `α` and non-negative `b` in `β`, `a₁ × b < a₂ × b` implies `a₁ < a₂`.
|
smul_le_smul_iff_of_neg
theorem smul_le_smul_iff_of_neg :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : OrderedRing α] [inst_1 : OrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : PosSMulMono α β] [inst_4 : PosSMulReflectLE α β],
a < 0 → (a • b₁ ≤ a • b₂ ↔ b₂ ≤ b₁)
This theorem, named `smul_le_smul_iff_of_neg`, is an alias of `smul_le_smul_iff_of_neg_left`. It describes a property of scalar multiplication in the context of ordered rings and ordered additive commutative groups. Specifically, for any negative scalar `a` and any two elements `b₁` and `b₂` from an ordered additive commutative group that is also a module over the ordered ring, the theorem states that `a` times `b₁` is less than or equal to `a` times `b₂` if and only if `b₂` is less than or equal to `b₁`. This mirrors the usual rule for inequalities involving negative numbers in elementary arithmetic, but in a more general algebraic setting.
More concisely: For any negative scalar `a` and elements `b₁` and `b₂` in an ordered additive commutative group that is also a module over an ordered ring, `a * b₁ <= a * b₂` if and only if `b₂ <= b₁`.
|
smul_lt_smul_of_pos
theorem smul_lt_smul_of_pos :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero α] [inst_4 : PosSMulStrictMono α β], b₁ < b₂ → 0 < a → a • b₁ < a • b₂
This theorem, `smul_lt_smul_of_pos`, is an alias of `smul_lt_smul_of_pos_left`. It states that, given any two types `α` and `β`, along with elements `a` of type `α` and `b₁, b₂` of type `β`, and assuming that `α` and `β` have a scalar multiplication operation, a preorder relation, a concept of zero, and a strictly monotonic positive scalar multiplication, then if `b₁` is less than `b₂` and `a` is positive, the result of scaling `b₁` by `a` will be less than the result of scaling `b₂` by `a`. In mathematical notation, this theorem asserts that if $b_1 < b_2$ and $0 < a$, then $a \cdot b_1 < a \cdot b_2$.
More concisely: Given types `α` and `β` with scalar multiplication, a preorder relation, zero, and strictly monotonic positive scalars, if `0 < a` and `b₁ < b₂` hold, then `a * b₁ < a * b₂`.
|
OrderIso.smulLeft_apply
theorem OrderIso.smulLeft_apply :
∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : MulAction α β] [inst_4 : PosSMulMono α β] [inst_5 : PosSMulReflectLE α β] {a : α} (ha : 0 < a) (b : β),
(OrderIso.smulRight ha) b = a • b
The theorem `OrderIso.smulLeft_apply` is an alternative version of `OrderIso.smulRight_apply`. It states that for any non-zero scalar `a` from a group with zero and any element `b` from a preordered set, where the scalar multiplication operation from `a` to `b` is defined and has the properties of monotonicity and reflection, when the `OrderIso.smulRight` function is applied to `b` with the scalar `a`, the result will be the same as directly applying the scalar multiplication of `a` and `b`. That is, `(OrderIso.smulRight a) b = a • b`.
More concisely: For any non-zero scalar `a` in a group and any element `b` in a preordered set with monotonic and reflective scalar multiplication, `OrderIso.smulRight a b = a * b`.
|
PosSMulStrictMono.elim
theorem PosSMulStrictMono.elim :
∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α]
[self : PosSMulStrictMono α β] ⦃a : α⦄, 0 < a → ∀ ⦃b₁ b₂ : β⦄, b₁ < b₂ → a • b₁ < a • b₂
This theorem, `PosSMulStrictMono.elim`, states that for any types `α` and `β` where `α` has an action on `β` (i.e., `β` is a module over `α`) and `α` and `β` are preordered (there is a less than relation that is transitive and reflexive) and `α` has a zero, then if `α` is strictly monotonically increasing when 'scaled' by positive elements (`PosSMulStrictMono`), for any positive `a` of type `α`, and any `b₁` and `b₂` of type `β` where `b₁` is less than `b₂`, the result of scaling `b₁` by `a` (denoted `a • b₁`) is less than the result of scaling `b₂` by `a` (denoted `a • b₂`). However, users are advised not to use this theorem directly and use `smul_lt_smul_of_pos_left` instead.
More concisely: For types `α` with a zero and preorder, and `β` as an `α`-module where `α` is strictly monotonically increasing when scaled by positives, for all positive `a` in `α` and `b₁` and `b₂` in `β` with `b₁ < b₂`, we have `a • b₁ < a • b₂`.
|
smul_lt_smul_iff_of_pos_left
theorem smul_lt_smul_iff_of_pos_left :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero α] [inst_4 : PosSMulStrictMono α β] [inst_5 : PosSMulReflectLT α β],
0 < a → (a • b₁ < a • b₂ ↔ b₁ < b₂)
The theorem `smul_lt_smul_iff_of_pos_left` states that for any types `α` and `β`, given a scalar multiplication operation `SMul α β`, a preordering on `α` and `β`, a zero element in `α`, and assuming positive scalar multiplication is strictly monotonic and reflects less than comparisons in `β`, if a scalar `a` is positive, then scalar multiplication by `a` preserves the order of `b₁` and `b₂`. In other words, `a • b₁` is less than `a • b₂` if and only if `b₁` is less than `b₂`.
More concisely: Given a commutative semigroup with zero `(α, ⊕, 0)`, a preorder `≤` on `α`, and a scalar multiplication `SMul α β` on `α × β` such that `a • b` is defined if and only if `a ≥ 0` and `b ≤ 0` or `a ≤ 0` and `b ≥ 0`, and `a • b₁ ≤ a • b₂` if and only if `b₁ ≤ b₂`, then `a > 0` implies `a • b₁ < a • b₂` whenever `b₁ < b₂`.
|
smul_add_smul_le_smul_add_smul
theorem smul_add_smul_le_smul_add_smul :
∀ {α : Type u_1} {β : Type u_2} [inst : OrderedRing α] [inst_1 : OrderedAddCommGroup β] [inst_2 : Module α β]
[inst_3 : PosSMulMono α β] [inst_4 : ContravariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{b₁ b₂ : α} {a d : β}, b₁ ≤ b₂ → a ≤ d → b₁ • d + b₂ • a ≤ b₁ • a + b₂ • d
This theorem is a statement of the binary **rearrangement inequality** in the context of an ordered ring and an ordered additive commutative group. For any two scalars `b₁` and `b₂` from the ordered ring and any two vectors `a` and `d` from the ordered additive commutative group, if `b₁` is less than or equal to `b₂` and `a` is less than or equal to `d`, then the sum of `b₁` times `d` and `b₂` times `a` is less than or equal to the sum of `b₁` times `a` and `b₂` times `d`.
In mathematical notation: for all $b_{1}, b_{2}$ in an ordered ring $α$ and all $a, d$ in an ordered additive commutative group $β$, if $b_{1} ≤ b_{2}$ and $a ≤ d$ then $b_{1}d + b_{2}a ≤ b_{1}a + b_{2}d$.
More concisely: For any ordered ring and ordered additive commutative group, if two scalars are in order and two vectors are in order with the first vector less than or equal to the second, then the dot product of the first scalar with the second vector, and the second scalar with the first vector, is less than or equal to the sum of the dot products of each scalar with its respective vector.
|
smul_pos_iff_of_pos
theorem smul_pos_iff_of_pos :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β]
[inst_3 : Preorder α] [inst_4 : Preorder β] [inst_5 : PosSMulStrictMono α β] [inst_6 : PosSMulReflectLT α β],
0 < a → (0 < a • b ↔ 0 < b)
The theorem `smul_pos_iff_of_pos` states that for any types `α` and `β`, given entities `a` of type `α` and `b` of type `β`, under the conditions that `α` and `β` are both ordered (i.e., they have a `Preorder` structure), and `α` and `β` form a scalar multiplication zero class (`SMulZeroClass`), a positive scalar multiplication strictly increasing monotonicity (`PosSMulStrictMono`) and a positive scalar multiplication reflects less than (`PosSMulReflectLT`), if `a` is positive, then `a` scaled by `b` is positive if and only if `b` is positive. In mathematical terms, it means that for all `0 < a`, the inequality `0 < a • b` holds if and only if `0 < b`.
More concisely: For types `α` and `β` with `Preorder` and `SMulZeroClass` structures, if `α` is ordered and `PosSMulStrictMono` and `PosSMulReflectLT` hold, then multiplication by a positive element of `α` strictly increases and preserves positivity in `β`, that is, `0 < a` implies `0 < a × b`.
|
smul_min
theorem smul_min :
∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : LinearOrder β]
[inst_3 : Zero α] [inst_4 : PosSMulMono α β], 0 ≤ a → ∀ (b₁ b₂ : β), a • min b₁ b₂ = min (a • b₁) (a • b₂)
This theorem, referred to as `smul_min`, states that for any types `α` and `β`, given an element `a` of type `α`, a scalar multiplication operation on `α` and `β`, a preorder structure on `α`, a linear order structure on `β`, a zero element in `α`, and a monotonically increasing scalar multiplication from `α` to `β`, if `a` is nonnegative, then for any two elements `b₁` and `b₂` of type `β`, multiplying `a` with the minimum of `b₁` and `b₂` results in the minimum of the results of multiplying `a` with `b₁` and `b₂` separately. In other words, the operation of scalar multiplication with a non-negative scalar distributes over the minimum operation.
More concisely: For any preorder type `α` with a zero element, scalar multiplication `smul` on `α` and `β`, and monotonically increasing `smul` from `α` to `β`, if `α` has a non-negative element `a` and `β` is linearly ordered, then `a * (min b₁ b₂) = min (a * b₁) (a * b₂)` for all `b₁, b₂ ∈ β`.
|
Mathlib.Algebra.Order.Module.Defs._auxLemma.19
theorem Mathlib.Algebra.Order.Module.Defs._auxLemma.19 :
∀ {ι : Type u} {α : ι → Type v} [inst : (i : ι) → Preorder (α i)] {x y : (i : ι) → α i},
(x < y) = (x ≤ y ∧ ∃ i, x i < y i)
This theorem, named `Mathlib.Algebra.Order.Module.Defs._auxLemma.19`, asserts that for any type `ι`, a function `α : ι → Type v` mapping `ι` to `Preorder`, and two instances `x` and `y` from `ι` to `α i`, `x` is less than `y` if and only if `x` is less than or equal to `y` and there exists an `i` such that `x i` is less than `y i`. Basically, it defines the "less than" relation in terms of "less than or equal to" relation and an existential quantification.
More concisely: For any preorder `α : ι → Type v`, and `x` and `y` in `ι` with types `α i` and `α j` respectively, `x` is less than `y` if and only if `x` is less than or equal to `y` and there exists some `i` such that `x i` is strictly less than `y i`.
|
smul_nonneg_iff_pos_imp_nonneg
theorem smul_nonneg_iff_pos_imp_nonneg :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedRing α] [inst_1 : LinearOrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : PosSMulStrictMono α β] {a : α} {b : β},
0 ≤ a • b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)
The theorem `smul_nonneg_iff_pos_imp_nonneg` states that for any types `α` and `β`, where `α` is a linearly ordered ring, `β` is a linearly ordered additive commutative group, and `β` is a module over `α` with strictly positive scalar multiplication, the scalar multiplication of `a` (an element of `α`) and `b` (an element of `β`) is non-negative if and only if when `a` is positive it implies `b` is non-negative, and `b` is positive it implies `a` is non-negative.
More concisely: For any linearly ordered ring `α`, linearly ordered additive commutative group `β` with strictly positive scalar multiplication, and `a` in `α` and `b` in `β`, the scalar multiplication `a * b` is non-negative if and only if `a` is positive implies `b` is non-negative, and `b` is positive implies `a` is non-negative.
|
smul_le_smul_of_nonpos
theorem smul_le_smul_of_nonpos :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : OrderedRing α] [inst_1 : OrderedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : PosSMulMono α β], b₁ ≤ b₂ → a ≤ 0 → a • b₂ ≤ a • b₁
This theorem, titled "smul_le_smul_of_nonpos", states that for any types `α` and `β`, given an ordered ring `α`, an ordered additive commutative group `β`, a module over `α` and `β`, and a positive scalar multiplication property on `α` and `β`, if `b₁` is less than or equal to `b₂` and `a` is less than or equal to zero, then the scalar multiplication of `a` and `b₂` is less than or equal to the scalar multiplication of `a` and `b₁`. It's an alias of the theorem `smul_le_smul_of_nonpos_left`.
More concisely: For any ordered ring `α`, ordered additive commutative group `β`, module `M` over `α` and `β`, and positive scalar multiplication on `α` and `β`, if `a ≤ 0` and `b₁ ≤ b₂`, then `a * b₂ ≤ a * b₁` in `M`.
|
monotone_smul_left
theorem monotone_smul_left :
∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero α] [inst_4 : PosSMulMono α β], 0 ≤ a → Monotone fun x => a • x
The theorem `monotone_smul_left` states that for any types `α` and `β` where `α` is a scalar and `β` is a vector (or more broadly, some item which can be scaled), given a non-negative scalar `a` (i.e., `0 ≤ a`) and the following instances: scalar multiplication (`SMul α β`), preorders on `α` and `β` (ensuring that `α` and `β` have a notion of order), a zero element in `α` (`Zero α`), and a property that multiplication by a positive scalar is monotone (`PosSMulMono α β`), then the function that scales any element `x` in `β` by `a` (i.e., the function `fun x => a • x`) is a monotone function. In other words, for all `x` and `y` in `β`, if `x ≤ y` then `a • x ≤ a • y`.
More concisely: Given types `α` and `β` with scalar multiplication, preorders, and a zero element, if `α` has monotone scalar multiplication by non-negative scalars, then scaling a vector `β` by a non-negative scalar results in a monotone function.
|
smul_add_smul_lt_smul_add_smul'
theorem smul_add_smul_lt_smul_add_smul' :
∀ {α : Type u_1} {β : Type u_2} [inst : OrderedRing α] [inst_1 : OrderedAddCommGroup β] [inst_2 : Module α β]
[inst_3 : PosSMulStrictMono α β] [inst_4 : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst_5 : ContravariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {b₁ b₂ : α} {a d : β},
b₂ < b₁ → d < a → b₁ • d + b₂ • a < b₁ • a + b₂ • d
The theorem `smul_add_smul_lt_smul_add_smul'` states a binary strict rearrangement inequality in the context of ordered rings and ordered additive commutative groups. Given two elements `b₁` and `b₂` from an ordered ring, and two elements `a` and `d` from an ordered additive commutative group such that `b₂ < b₁` and `d < a`, the sum of `b₁` scaled by `d` and `b₂` scaled by `a` (`b₁ • d + b₂ • a`) is strictly less than the sum of `b₁` scaled by `a` and `b₂` scaled by `d` (`b₁ • a + b₂ • d`). The 'scaling' is defined in the context of a module structure on the group. The theorem essentially expresses that rearranging the terms under these conditions preserves the strict inequality.
More concisely: Given elements `b₁ < b₂` in an ordered ring and `d < a` in an ordered additive commutative group, the scaling operation satisfies `b₁ • d + b₂ • a < b₁ • a + b₂ • d`.
|
strictMono_smul_left_of_pos
theorem strictMono_smul_left_of_pos :
∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero α] [inst_4 : PosSMulStrictMono α β], 0 < a → StrictMono fun x => a • x
The theorem `strictMono_smul_left_of_pos` states that for any types `α` and `β`, given a scalar `a` of type `α`, with `α` being a type on which scalar multiplication is defined and having a strict preorder structure, and `β` being a type with a preorder structure, also assuming `α` has a zero element and for any `α` and `β`, positive scalar multiplication is strictly monotone, if `a` is positive (i.e., greater than zero), then the function that multiplies every element of `β` by `a` is strictly monotone. The strict monotonicity means that if any element `b` is greater than an element `c`, then `a • b` is also greater than `a • c`.
More concisely: If `α` is a type with a strict preorder, scalar multiplication is strictly monotone on `α`, and `a` is a positive scalar in `α`, then the function that maps each element `x` in a type `β` with a preorder to `a * x` is strictly increasing.
|
le_of_smul_le_smul_of_pos_right
theorem le_of_smul_le_smul_of_pos_right :
∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero β] [inst_4 : SMulPosReflectLE α β], a₁ • b ≤ a₂ • b → 0 < b → a₁ ≤ a₂
This theorem, `le_of_smul_le_smul_of_pos_right`, states that for all types `α` and `β`, and for all elements `a₁`, `a₂` of type `α`, and `b` of type `β` where `SMul α β` (scalar multiplication between `α` and `β`), `Preorder α` (a preorder relation on `α`), `Preorder β` (a preorder relation on `β`), `Zero β` (a zero element in `β`) and `SMulPosReflectLE α β` (a positive reflection of scalar multiplication on `α` and `β`) are assumed, if `a₁ • b` is less than or equal to `a₂ • b` and `b` is positive, then `a₁` is less than or equal to `a₂`. In simple terms, this theorem states that in the given conditions if a scalar multiple of `b` by `a₁` is less than or equal to a scalar multiple of `b` by `a₂` and `b` is positive, then `a₁` is less than or equal to `a₂`.
More concisely: Given types `α` and `β` with preorders, scalar multiplication `SMul` between them, and positive reflection of inequality `SMulPosReflectLE`, if `a₁ • b` ≤ `a₂ • b` and `b` is positive, then `a₁` ≤ `a₂`.
|
le_of_smul_le_smul_of_pos_left
theorem le_of_smul_le_smul_of_pos_left :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero α] [inst_4 : PosSMulReflectLE α β], a • b₁ ≤ a • b₂ → 0 < a → b₁ ≤ b₂
The theorem `le_of_smul_le_smul_of_pos_left` states that, for any types `α` and `β`, given an instance of scalar multiplication (`SMul`) on `α` and `β`, preorder relationships on `α` and `β`, a zero element in `α`, and a property `PosSMulReflectLE` that reflects relation of `≤` across positive scalar multiplication, if the product of scalar `a` (where `a` is positive) and `β` value `b₁` is less than or equal to the product of `a` and another `β` value `b₂`, then `b₁` is less than or equal to `b₂`. In mathematical terms, for all positive `a`, if `a * b₁ ≤ a * b₂` then `b₁ ≤ b₂`.
More concisely: For all types α and β with scalar multiplication, and for all positive a, if a * b₁ ≤ a * b₂ then b₁ ≤ b₂.
|
smul_lt_smul_iff_of_pos
theorem smul_lt_smul_iff_of_pos :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero α] [inst_4 : PosSMulStrictMono α β] [inst_5 : PosSMulReflectLT α β],
0 < a → (a • b₁ < a • b₂ ↔ b₁ < b₂)
This theorem, `smul_lt_smul_iff_of_pos`, states that for any types `α` and `β`, any instance `a` of type `α`, and any instances `b₁` and `b₂` of type `β` given the conditions that `α` and `β` are ordered types, `α` has a zero, `α` and `β` have a scalar multiplication operation, and the scalar multiplication operation on `α` and `β` is strictly monotonic for positive `α` and reflects less than ordering, if `a` is greater than zero, then `a` times `b₁` is less than `a` times `b₂` if and only if `b₁` is less than `b₂`. In simple terms, it describes the property of scalar multiplication that preserves the order of elements when the scalar is positive.
More concisely: For any ordered types `α` and `β` with a zero, and having a strictly monotonic scalar multiplication operation that reflects order, if `a` is positive in `α` and `b₁ < b₂` in `β`, then `a * b₁ < a * b₂`.
|
le_of_smul_le_smul_left
theorem le_of_smul_le_smul_left :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero α] [inst_4 : PosSMulReflectLE α β], a • b₁ ≤ a • b₂ → 0 < a → b₁ ≤ b₂
This theorem, `le_of_smul_le_smul_left`, states that for any types `α` and `β`, given an instance of the `SMul α β` type class (indicating that elements of type `α` can scale elements of type `β`), instances of `Preorder α` and `Preorder β` (implying that both `α` and `β` have a "less than or equal to" relation), an instance of `Zero α` (indicating that `α` has a notion of zero), and an instance of `PosSMulReflectLE α β` (indicating that positive scaling reflects order in `β`), if `a • b₁` is less than or equal to `a • b₂` and `a` is greater than zero, then `b₁` is less than or equal to `b₂`. In other words, if one quantity scaled by a positive scalar is smaller or equal to another quantity scaled by the same scalar, then the original quantity is also smaller or equal to the other quantity.
More concisely: Given `α` and `β` types with `Preorder`, `SMul`, `Zero`, and `PosSMulReflectLE` instances, if `a > 0`, `a * b₁ ≤ a * b₂` implies `b₁ ≤ b₂`.
|
PosSMulReflectLT.of_pos
theorem PosSMulReflectLT.of_pos :
∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
[inst_3 : PartialOrder α] [inst_4 : Preorder β],
(∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂) → PosSMulReflectLT α β
The theorem `PosSMulReflectLT.of_pos` is a constructor for `PosSMulReflectLT`. It requires a proof that, for all types `α` and `β` where `α` has a zero, `β` has a zero, `α` can be scalar multiplied with `β` with zero, `α` has a partial order, and `β` has a preorder, if a scalar `a` is greater than zero, then for any `b₁` and `b₂` in `β`, if `a` scalar multiplied with `b₁` is less than `a` scalar multiplied with `b₂`, then `b₁` is less than `b₂`.
More concisely: Given types `α` and `β` with zeroes, scalar multiplication `α × β → α`, partial order on `α`, and preorder on `β`, if `a` is a positive scalar, then `a * b₁ < a * b₂` implies `b₁ < b₂`.
|
smul_le_smul_of_nonneg
theorem smul_le_smul_of_nonneg :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero α] [inst_4 : PosSMulMono α β], b₁ ≤ b₂ → 0 ≤ a → a • b₁ ≤ a • b₂
This theorem, `smul_le_smul_of_nonneg`, is an alias of `smul_le_smul_of_nonneg_left` and states that for any types `α` and `β`, any scalars `a` of type `α`, and any vectors `b₁` and `b₂` of type `β`, given a scalar multiplication (`SMul α β`), a preorder on `α` and `β`, a zero element of `α`, and a positive scalar multiplication monoid on `α` and `β`, if `b₁` is less than or equal to `b₂` and `a` is nonnegative, then the scalar multiplication of `a` and `b₁` is less than or equal to the scalar multiplication of `a` and `b₂`. This theorem is a generalization of the property of real numbers where if `b₁ ≤ b₂` and `a ≥ 0`, then `a * b₁ ≤ a * b₂`.
More concisely: For any types α and β, scalars a of type α, vectors b₁ and b₂ of type β, a preorder on α and β, a zero element of α, and a positive scalar multiplication monoid on α and β, if b₁ ≤ b₂ and a ≥ 0, then a * b₁ ≤ a * b₂.
|
OrderIso.smulLeft_symm_apply
theorem OrderIso.smulLeft_symm_apply :
∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : MulAction α β] [inst_4 : PosSMulMono α β] [inst_5 : PosSMulReflectLE α β] {a : α} (ha : 0 < a) (b : β),
(RelIso.symm (OrderIso.smulRight ha)) b = a⁻¹ • b
This theorem, `OrderIso.smulLeft_symm_apply`, states that for any types `α` and `β`, where `α` is a group with zero and `β` is under a multiplication action by `α` with certain properties (`PosSMulMono` and `PosSMulReflectLE`), and for any positive element `a` of `α` and any element `b` of `β`, the inverse of the order isomorphism defined by right scalar multiplication by `a` (given by `OrderIso.smulRight ha`) evaluated at `b` is equal to `b` scaled by the inverse of `a` (written as `a⁻¹ • b` in Lean notation).
More concisely: For any group `α` with zero, and any type `β` under multiaction by `α` satisfying `PosSMulMono` and `PosSMulReflectLE`, the order isomorphism from right scalar multiplication by a positive element `a` of `α` is the inverse of left scalar multiplication by `a`'s multiplicative inverse on elements of `β`.
|
PosSMulReflectLT.elim
theorem PosSMulReflectLT.elim :
∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α]
[self : PosSMulReflectLT α β] ⦃a : α⦄, 0 ≤ a → ∀ ⦃b₁ b₂ : β⦄, a • b₁ < a • b₂ → b₁ < b₂
This theorem, `PosSMulReflectLT.elim`, asserts the following: for any types 'α' and 'β' where 'α' is a scalar multiplication over 'β' and both are preordered, and given 'α' has a zero element, if 'a' is a non-negative scalar, then for any two elements 'b₁' and 'b₂' in 'β', if 'a' scaled by 'b₁' is less than 'a' scaled by 'b₂', it implies that 'b₁' is less than 'b₂'. However, this theorem should not be used. Instead, `lt_of_smul_lt_smul_left` should be used.
More concisely: If 'α' is a scalar multiplication over preordered type 'β' with a zero element, and 'a' is a non-negative scalar in 'α', then 'a * b₁' < 'a * b₂' implies 'b₁' < 'b₂'.
|
lt_of_smul_lt_smul_of_nonneg_left
theorem lt_of_smul_lt_smul_of_nonneg_left :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero α] [inst_4 : PosSMulReflectLT α β], a • b₁ < a • b₂ → 0 ≤ a → b₁ < b₂
This theorem, `lt_of_smul_lt_smul_of_nonneg_left`, states that for all types `α` and `β`, with variables `a` of type `α` and `b₁`, `b₂` of type `β`, given instances of scalar multiplication (`SMul α β`), preorders on `α` and `β`, zero for `α`, and positive scalar multiplication reflected in less-than relation (`PosSMulReflectLT α β`), if the scalar multiplication of `a` and `b₁` is less than the scalar multiplication of `a` and `b₂` and `a` is non-negative (greater or equal to zero), then `b₁` is less than `b₂`. This theorem is an alias of `lt_of_smul_lt_smul_left`.
More concisely: For all types `α` and `β`, if `a ∈ α` is non-negative and `a * b₁ < a * b₂` for scalars `b₁, b₂ ∈ β` with positive scalar multiplication and preorders on `α` and `β`, then `b₁ < b₂`.
|
smul_le_smul_iff_of_pos
theorem smul_le_smul_iff_of_pos :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
[inst_3 : Zero α] [inst_4 : PosSMulMono α β] [inst_5 : PosSMulReflectLE α β],
0 < a → (a • b₁ ≤ a • b₂ ↔ b₁ ≤ b₂)
This theorem, named `smul_le_smul_iff_of_pos`, states that for any types `α` and `β`, and any elements `a` of type `α` and `b₁`, `b₂` of type `β`, under the conditions that `α` and `β` support scalar multiplication (i.e., `α` is a scalar and `β` is a vector space), `α` and `β` have a preorder (i.e., a binary relation that is reflexive and transitive), `α` has a zero element, and positive scalar multiplication is monotone and reflects less than or equal to, if `a` is greater than zero, then `a` times `b₁` is less than or equal to `a` times `b₂` if and only if `b₁` is less than or equal to `b₂`. In mathematical notation: if $0 < a$, then $a \cdot b_1 \leq a \cdot b_2$ if and only if $b_1 \leq b_2$.
More concisely: For any scalar type `α` with zero element and vector space type `β`, if `a` is a positive element of `α` and `b₁ ≤ b₂` hold in `β`, then `a * b₁ ≤ a * b₂`.
|