Additional results about ordered Subtraction #

theorem AddHom.le_map_tsub {α : Type u_1} {β : Type u_2} [Preorder α] [Add α] [Sub α] [OrderedSub α] [Preorder β] [Add β] [Sub β] [OrderedSub β] (f : AddHom α β) (hf : Monotone ↑f) (a : α) (b : α) :

↑f a - ↑f b ≤ ↑f (a - b)

theorem le_mul_tsub {R : Type u_3} [Distrib R] [Preorder R] [Sub R] [OrderedSub R] [CovariantClass R R (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : R} {b : R} {c : R} :

a * b - a * c ≤ a * (b - c)

theorem le_tsub_mul {R : Type u_3} [CommSemiring R] [Preorder R] [Sub R] [OrderedSub R] [CovariantClass R R (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : R} {b : R} {c : R} :

a * c - b * c ≤ (a - b) * c

theorem OrderIso.map_tsub {M : Type u_3} {N : Type u_4} [Preorder M] [Add M] [Sub M] [OrderedSub M] [PartialOrder N] [Add N] [Sub N] [OrderedSub N] (e : M ≃o N) (h_add : ∀ (a b : M), ↑e (a + b) = ↑e a + ↑e b) (a : M) (b : M) :

↑e (a - b) = ↑e a - ↑e b

An order isomorphism between types with ordered subtraction preserves subtraction provided that it preserves addition.

theorem AddMonoidHom.le_map_tsub {α : Type u_1} {β : Type u_2} [Preorder α] [AddCommMonoid α] [Sub α] [OrderedSub α] [Preorder β] [AddCommMonoid β] [Sub β] [OrderedSub β] (f : α →+ β) (hf : Monotone ↑f) (a : α) (b : α) :

↑f a - ↑f b ≤ ↑f (a - b)