Lemmas about subtraction in unbundled canonically ordered monoids #
theorem
add_tsub_cancel_iff_le
{α : Type u_1}
[CanonicallyOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b : α}
:
theorem
tsub_add_cancel_iff_le
{α : Type u_1}
[CanonicallyOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b : α}
:
theorem
tsub_eq_zero_iff_le
{α : Type u_1}
[CanonicallyOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b : α}
:
theorem
tsub_eq_zero_of_le
{α : Type u_1}
[CanonicallyOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b : α}
:
Alias of the reverse direction of tsub_eq_zero_iff_le
.
theorem
tsub_self
{α : Type u_1}
[CanonicallyOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
(a : α)
:
theorem
tsub_le_self
{α : Type u_1}
[CanonicallyOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b : α}
:
theorem
zero_tsub
{α : Type u_1}
[CanonicallyOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
(a : α)
:
theorem
tsub_self_add
{α : Type u_1}
[CanonicallyOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
(a b : α)
:
theorem
tsub_pos_iff_not_le
{α : Type u_1}
[CanonicallyOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b : α}
:
theorem
tsub_pos_of_lt
{α : Type u_1}
[CanonicallyOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b : α}
(h : a < b)
:
theorem
tsub_lt_of_lt
{α : Type u_1}
[CanonicallyOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b c : α}
(h : a < b)
:
theorem
AddLECancellable.tsub_le_tsub_iff_left
{α : Type u_1}
[CanonicallyOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b c : α}
(ha : AddLECancellable a)
(hc : AddLECancellable c)
(h : c ≤ a)
:
theorem
AddLECancellable.tsub_right_inj
{α : Type u_1}
[CanonicallyOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b c : α}
(ha : AddLECancellable a)
(hb : AddLECancellable b)
(hc : AddLECancellable c)
(hba : b ≤ a)
(hca : c ≤ a)
:
Lemmas where addition is order-reflecting. #
theorem
tsub_le_tsub_iff_left
{α : Type u_1}
[CanonicallyOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b c : α}
[AddLeftReflectLE α]
(h : c ≤ a)
:
theorem
tsub_right_inj
{α : Type u_1}
[CanonicallyOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b c : α}
[AddLeftReflectLE α]
(hba : b ≤ a)
(hca : c ≤ a)
:
@[reducible, inline]
abbrev
CanonicallyOrderedAddCommMonoid.toAddCancelCommMonoid
(α : Type u_1)
[CanonicallyOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
[AddLeftReflectLE α]
:
A CanonicallyOrderedAddCommMonoid
with ordered subtraction and order-reflecting addition is
cancellative. This is not an instance as it would form a typeclass loop.
See note [reducible non-instances].
Instances For
Lemmas in a linearly canonically ordered monoid. #
@[simp]
theorem
tsub_pos_iff_lt
{α : Type u_1}
[CanonicallyLinearOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b : α}
:
theorem
tsub_eq_tsub_min
{α : Type u_1}
[CanonicallyLinearOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
(a b : α)
:
theorem
AddLECancellable.lt_tsub_iff_right
{α : Type u_1}
[CanonicallyLinearOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b c : α}
(hc : AddLECancellable c)
:
theorem
AddLECancellable.lt_tsub_iff_left
{α : Type u_1}
[CanonicallyLinearOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b c : α}
(hc : AddLECancellable c)
:
theorem
AddLECancellable.tsub_lt_tsub_iff_right
{α : Type u_1}
[CanonicallyLinearOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b c : α}
(hc : AddLECancellable c)
(h : c ≤ a)
:
theorem
AddLECancellable.tsub_lt_self
{α : Type u_1}
[CanonicallyLinearOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b : α}
(ha : AddLECancellable a)
(h₁ : 0 < a)
(h₂ : 0 < b)
:
theorem
AddLECancellable.tsub_lt_self_iff
{α : Type u_1}
[CanonicallyLinearOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b : α}
(ha : AddLECancellable a)
:
theorem
AddLECancellable.tsub_lt_tsub_iff_left_of_le
{α : Type u_1}
[CanonicallyLinearOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b c : α}
(ha : AddLECancellable a)
(hb : AddLECancellable b)
(h : b ≤ a)
:
See lt_tsub_iff_left_of_le_of_le
for a weaker statement in a partial order.
theorem
tsub_lt_tsub_iff_right
{α : Type u_1}
[CanonicallyLinearOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b c : α}
[AddLeftReflectLE α]
(h : c ≤ a)
:
This lemma also holds for ENNReal
, but we need a different proof for that.
theorem
tsub_lt_self
{α : Type u_1}
[CanonicallyLinearOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b : α}
[AddLeftReflectLE α]
:
@[simp]
theorem
tsub_lt_self_iff
{α : Type u_1}
[CanonicallyLinearOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b : α}
[AddLeftReflectLE α]
:
theorem
tsub_lt_tsub_iff_left_of_le
{α : Type u_1}
[CanonicallyLinearOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b c : α}
[AddLeftReflectLE α]
(h : b ≤ a)
:
See lt_tsub_iff_left_of_le_of_le
for a weaker statement in a partial order.
theorem
tsub_tsub_eq_min
{α : Type u_1}
[CanonicallyLinearOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
[AddLeftReflectLE α]
(a b : α)
:
Lemmas about max
and min
. #
theorem
tsub_add_eq_max
{α : Type u_1}
[CanonicallyLinearOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b : α}
:
theorem
add_tsub_eq_max
{α : Type u_1}
[CanonicallyLinearOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b : α}
:
theorem
tsub_min
{α : Type u_1}
[CanonicallyLinearOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b : α}
:
theorem
tsub_add_min
{α : Type u_1}
[CanonicallyLinearOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
{a b : α}
:
theorem
Even.tsub
{α : Type u_1}
[CanonicallyLinearOrderedAddCommMonoid α]
[Sub α]
[OrderedSub α]
[AddLeftReflectLE α]
{m n : α}
(hm : Even m)
(hn : Even n)
: