Documentation

Mathlib.Algebra.Order.Sub.Basic

Additional results about ordered Subtraction #

theorem AddHom.le_map_tsub {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst : Add α] [inst : Sub α] [inst : OrderedSub α] [inst : Preorder β] [inst : Add β] [inst : Sub β] [inst : OrderedSub β] (f : AddHom α β) (hf : Monotone f) (a : α) (b : α) :
f a - f b f (a - b)
theorem le_mul_tsub {R : Type u_1} [inst : Distrib R] [inst : Preorder R] [inst : Sub R] [inst : OrderedSub R] [inst : 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_1} [inst : CommSemiring R] [inst : Preorder R] [inst : Sub R] [inst : OrderedSub R] [inst : 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_1} {N : Type u_2} [inst : Preorder M] [inst : Add M] [inst : Sub M] [inst : OrderedSub M] [inst : PartialOrder N] [inst : Add N] [inst : Sub N] [inst : OrderedSub N] (e : M ≃o N) (h_add : ∀ (a b : M), (RelIso.toRelEmbedding e).toEmbedding (a + b) = (RelIso.toRelEmbedding e).toEmbedding a + (RelIso.toRelEmbedding e).toEmbedding b) (a : M) (b : M) :
(RelIso.toRelEmbedding e).toEmbedding (a - b) = (RelIso.toRelEmbedding e).toEmbedding a - (RelIso.toRelEmbedding e).toEmbedding b

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

Preorder #

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