Additional results about ordered Subtraction #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem add_hom.le_map_tsub {α : Type u_1} {β : Type u_2} [preorder α] [has_add α] [has_sub α] [has_ordered_sub α] [preorder β] [has_add β] [has_sub β] [has_ordered_sub β] (f : add_hom α β) (hf : monotone ⇑f) (a b : α) :

⇑f a - ⇑f b ≤ ⇑f (a - b)

theorem le_mul_tsub {R : Type u_1} [distrib R] [preorder R] [has_sub R] [has_ordered_sub R] [covariant_class R R has_mul.mul has_le.le] {a b c : R} :

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

theorem le_tsub_mul {R : Type u_1} [comm_semiring R] [preorder R] [has_sub R] [has_ordered_sub R] [covariant_class R R has_mul.mul has_le.le] {a b c : R} :

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

theorem order_iso.map_tsub {M : Type u_1} {N : Type u_2} [preorder M] [has_add M] [has_sub M] [has_ordered_sub M] [partial_order N] [has_add N] [has_sub N] [has_ordered_sub N] (e : M ≃o N) (h_add : ∀ (a b : M), ⇑e (a + b) = ⇑e a + ⇑e b) (a 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 add_monoid_hom.le_map_tsub {α : Type u_1} {β : Type u_2} [preorder α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] [preorder β] [add_comm_monoid β] [has_sub β] [has_ordered_sub β] (f : α →+ β) (hf : monotone ⇑f) (a b : α) :

⇑f a - ⇑f b ≤ ⇑f (a - b)