GCongr.algebraMap_le_algebraMap
theorem GCongr.algebraMap_le_algebraMap :
∀ {α : Type u_1} (β : Type u_2) [inst : OrderedCommSemiring α] [inst_1 : OrderedSemiring β] [inst_2 : Algebra α β]
[inst_3 : SMulPosMono α β] {a₁ a₂ : α}, a₁ ≤ a₂ → (algebraMap α β) a₁ ≤ (algebraMap α β) a₂
This theorem, `GCongr.algebraMap_le_algebraMap`, states that for any type `α` which is an ordered commutative semiring, and another type `β` which is an ordered semiring and for which there is an algebra structure and scalar multiplication is positive monotone, if we have two elements `a₁` and `a₂` from `α` such that `a₁` is less than or equal to `a₂`, then the result of applying the algebra map to `a₁` is also less than or equal to the result of applying the same algebra map to `a₂`. This version of the theorem is for use by `gcongr` since `gcongr` does not preprocess `Monotone` conclusions.
More concisely: For any ordered commutative semiring `α` and ordered semiring `β` with positive monotone scalar multiplication, if `α`'s algebra map preserves order and `a₁ ≤ a₂` in `α`, then the image of `a₁` under the algebra map is less than or equal to the image of `a₂`.
|
GCongr.algebraMap_lt_algebraMap
theorem GCongr.algebraMap_lt_algebraMap :
∀ {α : Type u_1} (β : Type u_2) [inst : OrderedCommSemiring α] [inst_1 : StrictOrderedSemiring β]
[inst_2 : Algebra α β] [inst_3 : SMulPosStrictMono α β] {a₁ a₂ : α},
a₁ < a₂ → (algebraMap α β) a₁ < (algebraMap α β) a₂
The theorem `GCongr.algebraMap_lt_algebraMap` states that for any given types $\alpha$ and $\beta$, where $\alpha$ is an ordered commutative semiring, $\beta$ is a strictly ordered semiring, and $\beta$ is also an algebra over $\alpha$ with strictly positive scalar multiplication, if $a_1$ and $a_2$ are elements of $\alpha$ such that $a_1 < a_2$, then the image of $a_1$ under the algebra map is less than the image of $a_2$. In other words, the algebra map preserves the order of elements from $\alpha$.
More concisely: Given an ordered commutative semiring $\alpha$, a strictly ordered semiring and algebra $\beta$ over $\alpha$ with strictly positive scalar multiplication, the algebra map from $\alpha$ to $\beta$ preserves the order relation, that is, if $a\_1 < a\_2$ in $\alpha$, then the image of $a\_1$ under the algebra map is strictly less than the image of $a\_2$.
|