Lemmas about subtraction in unbundled canonically ordered monoids #
theorem
AddHom.le_map_tsub
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Add α]
[Sub α]
[OrderedSub α]
[Preorder β]
[Add β]
[Sub β]
[OrderedSub β]
(f : AddHom α β)
(hf : Monotone (DFunLike.coe f))
(a b : α)
:
LE.le (HSub.hSub (DFunLike.coe f a) (DFunLike.coe f b)) (DFunLike.coe f (HSub.hSub a b))
theorem
le_mul_tsub
{R : Type u_3}
[Distrib R]
[Preorder R]
[Sub R]
[OrderedSub R]
[MulLeftMono R]
{a b c : R}
:
theorem
le_tsub_mul
{R : Type u_3}
[CommSemiring R]
[Preorder R]
[Sub R]
[OrderedSub R]
[MulLeftMono R]
{a b 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 : OrderIso M N)
(h_add : ∀ (a b : M), Eq (DFunLike.coe e (HAdd.hAdd a b)) (HAdd.hAdd (DFunLike.coe e a) (DFunLike.coe e b)))
(a b : M)
:
Eq (DFunLike.coe e (HSub.hSub a b)) (HSub.hSub (DFunLike.coe e a) (DFunLike.coe e b))
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 : AddMonoidHom α β)
(hf : Monotone (DFunLike.coe f))
(a b : α)
:
LE.le (HSub.hSub (DFunLike.coe f a) (DFunLike.coe f b)) (DFunLike.coe f (HSub.hSub a b))