OrderedSMul.smul_lt_smul_of_pos
theorem OrderedSMul.smul_lt_smul_of_pos :
∀ {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst_1 : OrderedAddCommMonoid M]
[inst_2 : SMulWithZero R M] [self : OrderedSMul R M] {a b : M} {c : R}, a < b → 0 < c → c • a < c • b
The theorem `OrderedSMul.smul_lt_smul_of_pos` states the following: for any given types `R` and `M`, where `R` is an ordered semiring, `M` is an ordered additive commutative monoid, and `M` has a scalar multiplication operation with zero from `R`, if we have an instance of the order-preserving scalar multiplication (`OrderedSMul`) property for `R` and `M`, then for any elements `a` and `b` of type `M` and an element `c` of type `R`, if `a` is less than `b` and `c` is greater than zero, then the result of multiplying `c` with `a` is less than the result of multiplying `c` with `b`. In essence, scalar multiplication by a positive element preserves the order of the elements in an ordered additive commutative monoid.
More concisely: If `R` is an ordered semiring, `M` is an ordered additive commutative monoid with scalar multiplication by elements of `R`, and `OrderedSMul` holds for `R` and `M`, then for all `a`, `b` in `M` and `c` in `R` with `a < b` and `c > 0`, `c * a < c * b`.
|
OrderedSMul.mk'
theorem OrderedSMul.mk' :
∀ {𝕜 : Type u_5} {M : Type u_7} [inst : LinearOrderedSemifield 𝕜] [inst_1 : OrderedAddCommMonoid M]
[inst_2 : MulActionWithZero 𝕜 M], (∀ ⦃a b : M⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b) → OrderedSMul 𝕜 M
The theorem `OrderedSMul.mk'` states that to establish an ordered scalar multiplication (`OrderedSMul`) structure over a vector space `M` with a linear ordered semifield `𝕜`, it's enough to confirm the first axiom of `OrderedSMul`. This axiom asserts that for all vectors `a` and `b` in `M` and a scalar `c` in `𝕜`, if `a` is less than `b` and `c` is greater than zero, then the scalar multiplication of `c` and `a` is less than or equal to the scalar multiplication of `c` and `b`.
More concisely: Given a vector space `M` over a linear ordered semifield `𝕜`, the ordered scalar multiplication structure holds if the first axiom (`a < b => c*a <= c*b` for all `a, b in M` and `c in 𝕜` with `c > 0`) is satisfied.
|
OrderedSMul.lt_of_smul_lt_smul_of_pos
theorem OrderedSMul.lt_of_smul_lt_smul_of_pos :
∀ {R : Type u_1} {M : Type u_2} [inst : OrderedSemiring R] [inst_1 : OrderedAddCommMonoid M]
[inst_2 : SMulWithZero R M] [self : OrderedSMul R M] {a b : M} {c : R}, c • a < c • b → 0 < c → a < b
This theorem states that, given an ordered semiring `R` and an ordered additive commutative monoid `M` endowed with an operation of scalar multiplication by elements of `R`, if the scalar multiplication of `a` by some positive `c` is less than the scalar multiplication of `b` by the same `c`, then `a` is less than `b`. In other words, if `c • a < c • b` for some positive `c`, then `a < b`.
More concisely: Given an ordered semiring `R` and an ordered additive commutative monoid `M` with scalar multiplication by `R`, if `c * a < c * b` for some positive `c` in `R`, then `a < b` in `M`.
|
OrderedSMul.mk''
theorem OrderedSMul.mk'' :
∀ {𝕜 : Type u_5} {M : Type u_7} [inst : OrderedSemiring 𝕜] [inst_1 : LinearOrderedAddCommMonoid M]
[inst_2 : SMulWithZero 𝕜 M], (∀ ⦃c : 𝕜⦄, 0 < c → StrictMono fun a => c • a) → OrderedSMul 𝕜 M
This theorem states that for any ordered semiring `𝕜` and any linear ordered additive commutative monoid `M`, if `M` is also a semimodule over `𝕜` where scalar multiplication with zero is defined, then `M` can be considered as an ordered semimodule over `𝕜` (denoted as `OrderedSMul 𝕜 M`) if the following condition holds: for any positive scalar `c` from `𝕜`, the function that maps each element `a` in `M` to the result of scaling `a` by `c` is strictly monotone. In other words, if increasing `a` always leads to an increase in `c • a` when `c` is positive, then an order-preserving scalar multiplication structure exists on `M`.
More concisely: If `𝕜` is an ordered semiring and `M` is an additive commutative monoid that is also a semimodule over `𝕜` with scalar multiplication by zero defined, then `M` is an ordered semimodule over `𝕜` if scalar multiplication by positive scalars is strictly monotone.
|