Additional results about ordered Subtraction #
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}
:
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 : α)
: