English
If e is an additive order isomorphism between two ordered subtraction structures, then e(a − b) = e(a) − e(b) whenever e preserves addition.
Русский
Если e — отображение по порядку, сохраняющее сложение между двумя структурами с упорядоченным вычитанием, то e(a − b) = e(a) − e(b), когда e сохраняет сложение.
LaTeX
$$$\forall a,b,\ e(a - b) = e(a) - e(b) \quad\text{whenever } e(a+b) = e(a) + e(b)$$$
Lean4
/-- An order isomorphism between types with ordered subtraction preserves subtraction provided that
it preserves addition. -/
theorem map_tsub {M N : Type*} [Preorder M] [Add M] [Sub M] [OrderedSub M] [PartialOrder N] [Add N] [Sub N]
[OrderedSub N] (e : M ≃o N) (h_add : ∀ a b, e (a + b) = e a + e b) (a b : M) : e (a - b) = e a - e b :=
by
let e_add : M ≃+ N := { e with map_add' := h_add }
refine le_antisymm ?_ (e_add.toAddHom.le_map_tsub e.monotone a b)
suffices e (e.symm (e a) - e.symm (e b)) ≤ e (e.symm (e a - e b)) by simpa
exact e.monotone (e_add.symm.toAddHom.le_map_tsub e.symm.monotone _ _)
