Lemmas about subtraction in unbundled canonically ordered monoids #
theorem
le_tsub_mul
{R : Type u_3}
[CommSemiring R]
[Preorder R]
[Sub R]
[OrderedSub R]
[CovariantClass R R (fun (x1 x2 : R) => x1 * x2) fun (x1 x2 : R) => x1 ≤ x2]
{a : R}
{b : R}
{c : R}
:
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)
:
An order isomorphism between types with ordered subtraction preserves subtraction provided that it preserves addition.
Preorder #
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 : α)
: