AddHom.le_map_tsub
theorem AddHom.le_map_tsub :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
[inst_4 : Preorder β] [inst_5 : Add β] [inst_6 : Sub β] [inst_7 : OrderedSub β] (f : AddHom α β),
Monotone ⇑f → ∀ (a b : α), f a - f b ≤ f (a - b)
The theorem `AddHom.le_map_tsub` asserts that for any types `α` and `β` with `Preorder`, `Add`, `Sub` and `OrderedSub` instances, and an additive homomorphism `f` from `α` to `β` that is monotone, for any elements `a` and `b` in `α`, the difference of `f(a)` and `f(b)` is less than or equal to `f(a - b)`. That is, if `f` preserves the order and addition operations, then it also preserves the subtraction in the sense of this inequality.
More concisely: If `f` is an additive, monotone homomorphism between preordered types `α` and `β`, then for all `a, b` in `α`, `f(a - b) ≤ f(a) - f(b)`.
|
OrderIso.map_tsub
theorem OrderIso.map_tsub :
∀ {M : Type u_3} {N : Type u_4} [inst : Preorder M] [inst_1 : Add M] [inst_2 : Sub M] [inst_3 : OrderedSub M]
[inst_4 : PartialOrder N] [inst_5 : Add N] [inst_6 : Sub N] [inst_7 : OrderedSub N] (e : M ≃o N),
(∀ (a b : M), e (a + b) = e a + e b) → ∀ (a b : M), e (a - b) = e a - e b
The theorem `OrderIso.map_tsub` states that for any two types `M` and `N` that have an ordered subtraction operation and an addition operation, if there exists an order isomorphism `e` between these types that preserves addition (i.e., applying `e` to the sum of two elements of `M` yields the sum of the `e`-images of these elements in `N`), then `e` also preserves the subtraction operation (i.e., subtracting two elements of `M` and then applying `e` to the result gives the same value as subtracting the `e`-images of these elements in `N`).
More concisely: If `e` is an order isomorphism between types `M` and `N` that preserves addition, then `e` also preserves subtraction. That is, for all `x` and `y` in `M`, `e(x - y) = e(x) - e(y)` holds.
|