Lemmas about subtraction in canonically ordered monoids #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[simp]
theorem
add_tsub_cancel_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b : α}
(h : a ≤ b) :
theorem
tsub_add_cancel_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b : α}
(h : a ≤ b) :
theorem
add_le_of_le_tsub_right_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(h : b ≤ c)
(h2 : a ≤ c - b) :
theorem
add_le_of_le_tsub_left_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(h : a ≤ c)
(h2 : b ≤ c - a) :
theorem
tsub_le_tsub_iff_right
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(h : c ≤ b) :
theorem
tsub_left_inj
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(h1 : c ≤ a)
(h2 : c ≤ b) :
theorem
tsub_inj_left
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(h₁ : a ≤ b)
(h₂ : a ≤ c) :
theorem
lt_of_tsub_lt_tsub_right_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(h : c ≤ b)
(h2 : a - c < b - c) :
a < b
See lt_of_tsub_lt_tsub_right for a stronger statement in a linear order.
theorem
tsub_add_tsub_cancel
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(hab : b ≤ a)
(hcb : c ≤ b) :
theorem
tsub_tsub_tsub_cancel_right
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(h : c ≤ b) :
Lemmas that assume that an element is add_le_cancellable. #
@[protected]
theorem
add_le_cancellable.eq_tsub_iff_add_eq_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(hc : add_le_cancellable c)
(h : c ≤ b) :
@[protected]
theorem
add_le_cancellable.tsub_eq_iff_eq_add_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(hb : add_le_cancellable b)
(h : b ≤ a) :
@[protected]
theorem
add_le_cancellable.add_tsub_assoc_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{b c : α}
(hc : add_le_cancellable c)
(h : c ≤ b)
(a : α) :
@[protected]
theorem
add_le_cancellable.tsub_add_eq_add_tsub
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(hb : add_le_cancellable b)
(h : b ≤ a) :
@[protected]
theorem
add_le_cancellable.tsub_tsub_assoc
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(hbc : add_le_cancellable (b - c))
(h₁ : b ≤ a)
(h₂ : c ≤ b) :
@[protected]
theorem
add_le_cancellable.tsub_add_tsub_comm
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c d : α}
(hb : add_le_cancellable b)
(hd : add_le_cancellable d)
(hba : b ≤ a)
(hdc : d ≤ c) :
@[protected]
theorem
add_le_cancellable.le_tsub_iff_left
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(ha : add_le_cancellable a)
(h : a ≤ c) :
@[protected]
theorem
add_le_cancellable.le_tsub_iff_right
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(ha : add_le_cancellable a)
(h : a ≤ c) :
@[protected]
theorem
add_le_cancellable.tsub_lt_iff_left
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(hb : add_le_cancellable b)
(hba : b ≤ a) :
@[protected]
theorem
add_le_cancellable.tsub_lt_iff_right
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(hb : add_le_cancellable b)
(hba : b ≤ a) :
@[protected]
theorem
add_le_cancellable.tsub_lt_iff_tsub_lt
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(hb : add_le_cancellable b)
(hc : add_le_cancellable c)
(h₁ : b ≤ a)
(h₂ : c ≤ a) :
@[protected]
theorem
add_le_cancellable.le_tsub_iff_le_tsub
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(ha : add_le_cancellable a)
(hc : add_le_cancellable c)
(h₁ : a ≤ b)
(h₂ : c ≤ b) :
@[protected]
theorem
add_le_cancellable.lt_tsub_iff_right_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(hc : add_le_cancellable c)
(h : c ≤ b) :
@[protected]
theorem
add_le_cancellable.lt_tsub_iff_left_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(hc : add_le_cancellable c)
(h : c ≤ b) :
@[protected]
theorem
add_le_cancellable.tsub_inj_right
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(hab : add_le_cancellable (a - b))
(h₁ : b ≤ a)
(h₂ : c ≤ a)
(h₃ : a - b = a - c) :
b = c
@[protected]
theorem
add_le_cancellable.lt_of_tsub_lt_tsub_left_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_lt.lt]
(hb : add_le_cancellable b)
(hca : c ≤ a)
(h : a - b < a - c) :
c < b
@[protected]
theorem
add_le_cancellable.tsub_lt_tsub_left_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(hab : add_le_cancellable (a - b))
(h₁ : b ≤ a)
(h : c < b) :
@[protected]
theorem
add_le_cancellable.tsub_lt_tsub_right_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(hc : add_le_cancellable c)
(h : c ≤ a)
(h2 : a < b) :
@[protected]
theorem
add_le_cancellable.tsub_lt_tsub_iff_left_of_le_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_lt.lt]
(hb : add_le_cancellable b)
(hab : add_le_cancellable (a - b))
(h₁ : b ≤ a)
(h₂ : c ≤ a) :
@[protected, simp]
theorem
add_le_cancellable.add_tsub_tsub_cancel
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(hac : add_le_cancellable (a - c))
(h : c ≤ a) :
@[protected]
theorem
add_le_cancellable.tsub_tsub_cancel_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b : α}
(hba : add_le_cancellable (b - a))
(h : a ≤ b) :
@[protected]
theorem
add_le_cancellable.tsub_tsub_tsub_cancel_left
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(hab : add_le_cancellable (a - b))
(h : b ≤ a) :
Lemmas where addition is order-reflecting. #
theorem
eq_tsub_iff_add_eq_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(h : c ≤ b) :
theorem
tsub_eq_iff_eq_add_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(h : b ≤ a) :
theorem
add_tsub_assoc_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{b c : α}
[contravariant_class α α has_add.add has_le.le]
(h : c ≤ b)
(a : α) :
See add_tsub_le_assoc for an inequality.
theorem
tsub_add_eq_add_tsub
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(h : b ≤ a) :
theorem
tsub_tsub_assoc
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(h₁ : b ≤ a)
(h₂ : c ≤ b) :
theorem
tsub_add_tsub_comm
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c d : α}
[contravariant_class α α has_add.add has_le.le]
(hba : b ≤ a)
(hdc : d ≤ c) :
theorem
le_tsub_iff_left
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(h : a ≤ c) :
theorem
le_tsub_iff_right
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(h : a ≤ c) :
theorem
tsub_lt_iff_left
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(hbc : b ≤ a) :
theorem
tsub_lt_iff_right
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(hbc : b ≤ a) :
theorem
tsub_lt_iff_tsub_lt
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(h₁ : b ≤ a)
(h₂ : c ≤ a) :
theorem
le_tsub_iff_le_tsub
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(h₁ : a ≤ b)
(h₂ : c ≤ b) :
theorem
lt_tsub_iff_right_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(h : c ≤ b) :
See lt_tsub_iff_right for a stronger statement in a linear order.
theorem
lt_tsub_iff_left_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(h : c ≤ b) :
See lt_tsub_iff_left for a stronger statement in a linear order.
theorem
lt_of_tsub_lt_tsub_left_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
[contravariant_class α α has_add.add has_lt.lt]
(hca : c ≤ a)
(h : a - b < a - c) :
c < b
See lt_of_tsub_lt_tsub_left for a stronger statement in a linear order.
theorem
tsub_lt_tsub_left_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le] :
theorem
tsub_lt_tsub_right_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(h : c ≤ a)
(h2 : a < b) :
theorem
tsub_inj_right
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(h₁ : b ≤ a)
(h₂ : c ≤ a)
(h₃ : a - b = a - c) :
b = c
theorem
tsub_lt_tsub_iff_left_of_le_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
[contravariant_class α α has_add.add has_lt.lt]
(h₁ : b ≤ a)
(h₂ : c ≤ a) :
See tsub_lt_tsub_iff_left_of_le for a stronger statement in a linear order.
@[simp]
theorem
add_tsub_tsub_cancel
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(h : c ≤ a) :
theorem
tsub_tsub_cancel_of_le
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b : α}
[contravariant_class α α has_add.add has_le.le]
(h : a ≤ b) :
See tsub_tsub_le for an inequality.
theorem
tsub_tsub_tsub_cancel_left
{α : Type u_1}
[add_comm_semigroup α]
[partial_order α]
[has_exists_add_of_le α]
[covariant_class α α has_add.add has_le.le]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(h : b ≤ a) :
Lemmas in a canonically ordered monoid. #
theorem
add_tsub_cancel_iff_le
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
theorem
tsub_add_cancel_iff_le
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
@[simp]
theorem
tsub_eq_zero_iff_le
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
@[simp]
theorem
tsub_eq_zero_of_le
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
Alias of the reverse direction of tsub_eq_zero_iff_le.
@[simp]
theorem
tsub_self
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
(a : α) :
@[simp]
theorem
tsub_le_self
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
@[simp]
theorem
zero_tsub
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
(a : α) :
theorem
tsub_self_add
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
(a b : α) :
theorem
tsub_pos_iff_not_le
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
theorem
tsub_pos_of_lt
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α}
(h : a < b) :
theorem
tsub_lt_of_lt
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(h : a < b) :
@[protected]
theorem
add_le_cancellable.tsub_le_tsub_iff_left
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(ha : add_le_cancellable a)
(hc : add_le_cancellable c)
(h : c ≤ a) :
@[protected]
theorem
add_le_cancellable.tsub_right_inj
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(ha : add_le_cancellable a)
(hb : add_le_cancellable b)
(hc : add_le_cancellable c)
(hba : b ≤ a)
(hca : c ≤ a) :
Lemmas where addition is order-reflecting. #
theorem
tsub_le_tsub_iff_left
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(h : c ≤ a) :
theorem
tsub_right_inj
{α : Type u_1}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(hba : b ≤ a)
(hca : c ≤ a) :
@[reducible]
def
canonically_ordered_add_monoid.to_add_cancel_comm_monoid
(α : Type u_1)
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
[contravariant_class α α has_add.add has_le.le] :
A canonically_ordered_add_monoid with ordered subtraction and order-reflecting addition is
cancellative. This is not an instance at it would form a typeclass loop.
See note [reducible non-instances].
Equations
- canonically_ordered_add_monoid.to_add_cancel_comm_monoid α = {add := add_comm_monoid.add (ordered_add_comm_monoid.to_add_comm_monoid α), add_assoc := _, add_left_cancel := _, zero := add_comm_monoid.zero (ordered_add_comm_monoid.to_add_comm_monoid α), zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul (ordered_add_comm_monoid.to_add_comm_monoid α), nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
Lemmas in a linearly canonically ordered monoid. #
@[simp]
theorem
tsub_pos_iff_lt
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
theorem
tsub_eq_tsub_min
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
(a b : α) :
a - b = a - linear_order.min a b
@[protected]
theorem
add_le_cancellable.lt_tsub_iff_right
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(hc : add_le_cancellable c) :
@[protected]
theorem
add_le_cancellable.lt_tsub_iff_left
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(hc : add_le_cancellable c) :
@[protected]
theorem
add_le_cancellable.tsub_lt_tsub_iff_right
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(hc : add_le_cancellable c)
(h : c ≤ a) :
@[protected]
theorem
add_le_cancellable.tsub_lt_self
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α}
(ha : add_le_cancellable a)
(h₁ : 0 < a)
(h₂ : 0 < b) :
@[protected]
theorem
add_le_cancellable.tsub_lt_self_iff
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α}
(ha : add_le_cancellable a) :
@[protected]
theorem
add_le_cancellable.tsub_lt_tsub_iff_left_of_le
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
(ha : add_le_cancellable a)
(hb : add_le_cancellable 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}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(h : c ≤ a) :
This lemma also holds for ennreal, but we need a different proof for that.
theorem
tsub_lt_self
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α}
[contravariant_class α α has_add.add has_le.le] :
theorem
tsub_lt_self_iff
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α}
[contravariant_class α α has_add.add has_le.le] :
theorem
tsub_lt_tsub_iff_left_of_le
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b c : α}
[contravariant_class α α has_add.add has_le.le]
(h : b ≤ a) :
See lt_tsub_iff_left_of_le_of_le for a weaker statement in a partial order.
Lemmas about max and min. #
theorem
tsub_add_eq_max
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
a - b + b = linear_order.max a b
theorem
add_tsub_eq_max
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
a + (b - a) = linear_order.max a b
theorem
tsub_min
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
a - linear_order.min a b = a - b
theorem
tsub_add_min
{α : Type u_1}
[canonically_linear_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
{a b : α} :
a - b + linear_order.min a b = a