Mathlib.Algebra.Order.Sub.Unbundled.Basic

add_tsub_cancel_of_le theorem

(h : a ≤ b) : a + (b - a) = b

Full source

@[simp]
theorem add_tsub_cancel_of_le (h : a ≤ b) : a + (b - a) = b := by
  refine le_antisymm ?_ le_add_tsub
  obtain ⟨c, rfl⟩ := exists_add_of_le h
  exact add_le_add_left add_tsub_le_left a

Cancellation of Subtraction in Ordered Monoid: $a + (b - a) = b$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid, if $a \leq b$, then $a + (b - a) = b$.

tsub_add_cancel_of_le theorem

(h : a ≤ b) : b - a + a = b

Full source

theorem tsub_add_cancel_of_le (h : a ≤ b) : b - a + a = b := by
  rw [add_comm]
  exact add_tsub_cancel_of_le h

Subtraction-Add Cancellation in Ordered Monoid: $(b - a) + a = b$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid, if $a \leq b$, then $(b - a) + a = b$.

add_le_of_le_tsub_right_of_le theorem

(h : b ≤ c) (h2 : a ≤ c - b) : a + b ≤ c

Full source

theorem add_le_of_le_tsub_right_of_le (h : b ≤ c) (h2 : a ≤ c - b) : a + b ≤ c :=
  (add_le_add_right h2 b).trans_eq <| tsub_add_cancel_of_le h

Addition Inequality via Right Subtraction: $a + b \leq c$ when $b \leq c$ and $a \leq c - b$

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $b \leq c$ and $a \leq c - b$, then $a + b \leq c$.

add_le_of_le_tsub_left_of_le theorem

(h : a ≤ c) (h2 : b ≤ c - a) : a + b ≤ c

Full source

theorem add_le_of_le_tsub_left_of_le (h : a ≤ c) (h2 : b ≤ c - a) : a + b ≤ c :=
  (add_le_add_left h2 a).trans_eq <| add_tsub_cancel_of_le h

Addition Inequality via Left Subtraction: $a + b \leq c$ when $a \leq c$ and $b \leq c - a$

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $a \leq c$ and $b \leq c - a$, then $a + b \leq c$.

tsub_le_tsub_iff_right theorem

(h : c ≤ b) : a - c ≤ b - c ↔ a ≤ b

Full source

theorem tsub_le_tsub_iff_right (h : c ≤ b) : a - c ≤ b - c ↔ a ≤ b := by
  rw [tsub_le_iff_right, tsub_add_cancel_of_le h]

Right Subtraction Preserves Order: $a - c \leq b - c \leftrightarrow a \leq b$ when $c \leq b$

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $c \leq b$, then the inequality $a - c \leq b - c$ holds if and only if $a \leq b$.

tsub_left_inj theorem

(h1 : c ≤ a) (h2 : c ≤ b) : a - c = b - c ↔ a = b

Full source

theorem tsub_left_inj (h1 : c ≤ a) (h2 : c ≤ b) : a - c = b - c ↔ a = b := by
  simp_rw [le_antisymm_iff, tsub_le_tsub_iff_right h1, tsub_le_tsub_iff_right h2]

Left Subtraction Injective: $a - c = b - c \leftrightarrow a = b$ when $c \leq a$ and $c \leq b$

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $c \leq a$ and $c \leq b$, then $a - c = b - c$ if and only if $a = b$.

tsub_inj_left theorem

(h₁ : a ≤ b) (h₂ : a ≤ c) : b - a = c - a → b = c

Full source

theorem tsub_inj_left (h₁ : a ≤ b) (h₂ : a ≤ c) : b - a = c - a → b = c :=
  (tsub_left_inj h₁ h₂).1

Left Subtraction Injective Implication: $b - a = c - a \Rightarrow b = c$ under $a \leq b$ and $a \leq c$

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $a \leq b$ and $a \leq c$, then the equality $b - a = c - a$ implies $b = c$.

lt_of_tsub_lt_tsub_right_of_le theorem

(h : c ≤ b) (h2 : a - c < b - c) : a < b

Full source

/-- See `lt_of_tsub_lt_tsub_right` for a stronger statement in a linear order. -/
theorem lt_of_tsub_lt_tsub_right_of_le (h : c ≤ b) (h2 : a - c < b - c) : a < b := by
  refine ((tsub_le_tsub_iff_right h).mp h2.le).lt_of_ne ?_
  rintro rfl
  exact h2.false

Strict Order from Right Subtraction: $a - c < b - c \Rightarrow a < b$ when $c \leq b$

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $c \leq b$ and $a - c < b - c$, then $a < b$.

tsub_add_tsub_cancel theorem

(hab : b ≤ a) (hcb : c ≤ b) : a - b + (b - c) = a - c

Full source

theorem tsub_add_tsub_cancel (hab : b ≤ a) (hcb : c ≤ b) : a - b + (b - c) = a - c := by
  convert tsub_add_cancel_of_le (tsub_le_tsub_right hab c) using 2
  rw [tsub_tsub, add_tsub_cancel_of_le hcb]

Subtraction-Add Cancellation Chain: $(a - b) + (b - c) = a - c$ under $c \leq b \leq a$

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $b \leq a$ and $c \leq b$, then $(a - b) + (b - c) = a - c$.

tsub_tsub_tsub_cancel_right theorem

(h : c ≤ b) : a - c - (b - c) = a - b

Full source

theorem tsub_tsub_tsub_cancel_right (h : c ≤ b) : a - c - (b - c) = a - b := by
  rw [tsub_tsub, add_tsub_cancel_of_le h]

Nested Subtraction Cancellation: $(a - c) - (b - c) = a - b$ when $c \leq b$

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $c \leq b$, then $(a - c) - (b - c) = a - b$.

AddLECancellable.tsub_eq_iff_eq_add_of_le theorem

(hb : AddLECancellable b) (h : b ≤ a) : a - b = c ↔ a = c + b

Full source

protected theorem tsub_eq_iff_eq_add_of_le (hb : AddLECancellable b) (h : b ≤ a) :
    a - b = c ↔ a = c + b := by rw [eq_comm, hb.eq_tsub_iff_add_eq_of_le h, eq_comm]

Subtraction Equivalence in Additively Left Cancellable Monoids: $a - b = c \leftrightarrow a = c + b$

Informal description

Let $a$, $b$, and $c$ be elements of a canonically ordered monoid. If $b$ is additively left cancellable and $b \leq a$, then the subtraction $a - b$ equals $c$ if and only if $a$ equals $c + b$.

AddLECancellable.add_tsub_assoc_of_le theorem

(hc : AddLECancellable c) (h : c ≤ b) (a : α) : a + b - c = a + (b - c)

Full source

protected theorem add_tsub_assoc_of_le (hc : AddLECancellable c) (h : c ≤ b) (a : α) :
    a + b - c = a + (b - c) := by
  conv_lhs => rw [← add_tsub_cancel_of_le h, add_comm c, ← add_assoc, hc.add_tsub_cancel_right]

Associativity of Addition and Subtraction in Additively Left Cancellable Monoids: $(a + b) - c = a + (b - c)$ when $c \leq b$

Informal description

Let $a$, $b$, and $c$ be elements of a canonically ordered monoid. If $c$ is additively left cancellable and $c \leq b$, then $(a + b) - c = a + (b - c)$.

AddLECancellable.tsub_add_eq_add_tsub theorem

(hb : AddLECancellable b) (h : b ≤ a) : a - b + c = a + c - b

Full source

protected theorem tsub_add_eq_add_tsub (hb : AddLECancellable b) (h : b ≤ a) :
    a - b + c = a + c - b := by rw [add_comm a, hb.add_tsub_assoc_of_le h, add_comm]

Subtraction-Add Commutativity in Additively Left Cancellable Monoids: $(a - b) + c = (a + c) - b$ when $b \leq a$

Informal description

Let $a$, $b$, and $c$ be elements of a canonically ordered monoid. If $b$ is additively left cancellable and $b \leq a$, then $(a - b) + c = (a + c) - b$.

AddLECancellable.tsub_tsub_assoc theorem

(hbc : AddLECancellable (b - c)) (h₁ : b ≤ a) (h₂ : c ≤ b) : a - (b - c) = a - b + c

Full source

protected theorem tsub_tsub_assoc (hbc : AddLECancellable (b - c)) (h₁ : b ≤ a) (h₂ : c ≤ b) :
    a - (b - c) = a - b + c :=
  hbc.tsub_eq_of_eq_add <| by rw [add_assoc, add_tsub_cancel_of_le h₂, tsub_add_cancel_of_le h₁]

Associativity of Double Subtraction in Additively Left Cancellable Monoids: $a - (b - c) = a - b + c$ when $b \leq a$ and $c \leq b$

Informal description

Let $a$, $b$, and $c$ be elements of a canonically ordered monoid. If $b - c$ is additively left cancellable, $b \leq a$, and $c \leq b$, then $a - (b - c) = a - b + c$.

AddLECancellable.tsub_add_tsub_comm theorem

(hb : AddLECancellable b) (hd : AddLECancellable d) (hba : b ≤ a) (hdc : d ≤ c) : a - b + (c - d) = a + c - (b + d)

Full source

protected theorem tsub_add_tsub_comm (hb : AddLECancellable b) (hd : AddLECancellable d)
    (hba : b ≤ a) (hdc : d ≤ c) : a - b + (c - d) = a + c - (b + d) := by
  rw [hb.tsub_add_eq_add_tsub hba, ← hd.add_tsub_assoc_of_le hdc, tsub_tsub, add_comm d]

Subtraction-Add Commutativity for Pairs in Additively Left Cancellable Monoids: $(a - b) + (c - d) = (a + c) - (b + d)$ when $b \leq a$ and $d \leq c$

Informal description

Let $a$, $b$, $c$, and $d$ be elements of a canonically ordered monoid. If $b$ and $d$ are additively left cancellable, $b \leq a$, and $d \leq c$, then $(a - b) + (c - d) = (a + c) - (b + d)$.

AddLECancellable.le_tsub_iff_left theorem

(ha : AddLECancellable a) (h : a ≤ c) : b ≤ c - a ↔ a + b ≤ c

Full source

protected theorem le_tsub_iff_left (ha : AddLECancellable a) (h : a ≤ c) : b ≤ c - a ↔ a + b ≤ c :=
  ⟨add_le_of_le_tsub_left_of_le h, ha.le_tsub_of_add_le_left⟩

Left Cancellable Subtraction Inequality: $b \leq c - a \leftrightarrow a + b \leq c$

Informal description

Let $a$, $b$, and $c$ be elements in a canonically ordered monoid, and suppose $a$ is additively left cancellable (i.e., $a + b \leq a + c$ implies $b \leq c$). If $a \leq c$, then $b \leq c - a$ if and only if $a + b \leq c$.

AddLECancellable.le_tsub_iff_right theorem

(ha : AddLECancellable a) (h : a ≤ c) : b ≤ c - a ↔ b + a ≤ c

Full source

protected theorem le_tsub_iff_right (ha : AddLECancellable a) (h : a ≤ c) :
    b ≤ c - a ↔ b + a ≤ c := by
  rw [add_comm]
  exact ha.le_tsub_iff_left h

Right Cancellable Subtraction Inequality: $b \leq c - a \leftrightarrow b + a \leq c$

Informal description

Let $a$, $b$, and $c$ be elements in a canonically ordered monoid, and suppose $a$ is additively left cancellable (i.e., $a + x \leq a + y$ implies $x \leq y$). If $a \leq c$, then $b \leq c - a$ if and only if $b + a \leq c$.

AddLECancellable.tsub_lt_iff_left theorem

(hb : AddLECancellable b) (hba : b ≤ a) : a - b < c ↔ a < b + c

Full source

protected theorem tsub_lt_iff_left (hb : AddLECancellable b) (hba : b ≤ a) :
    a - b < c ↔ a < b + c := by
  refine ⟨hb.lt_add_of_tsub_lt_left, ?_⟩
  intro h; refine (tsub_le_iff_left.mpr h.le).lt_of_ne ?_
  rintro rfl; exact h.ne' (add_tsub_cancel_of_le hba)

Left Cancellable Subtraction Inequality: $a - b < c \leftrightarrow a < b + c$

Informal description

Let $a$, $b$, and $c$ be elements in a canonically ordered monoid, and suppose $b$ is additively left cancellable (i.e., $b + x \leq b + y$ implies $x \leq y$). If $b \leq a$, then $a - b < c$ if and only if $a < b + c$.

AddLECancellable.tsub_lt_iff_right theorem

(hb : AddLECancellable b) (hba : b ≤ a) : a - b < c ↔ a < c + b

Full source

protected theorem tsub_lt_iff_right (hb : AddLECancellable b) (hba : b ≤ a) :
    a - b < c ↔ a < c + b := by
  rw [add_comm]
  exact hb.tsub_lt_iff_left hba

Right Cancellable Subtraction Inequality: $a - b < c \leftrightarrow a < c + b$

Informal description

Let $a$, $b$, and $c$ be elements in a canonically ordered monoid, and suppose $b$ is additively left cancellable (i.e., $b + x \leq b + y$ implies $x \leq y$). If $b \leq a$, then $a - b < c$ if and only if $a < c + b$.

AddLECancellable.tsub_lt_iff_tsub_lt theorem

(hb : AddLECancellable b) (hc : AddLECancellable c) (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < c ↔ a - c < b

Full source

protected theorem tsub_lt_iff_tsub_lt (hb : AddLECancellable b) (hc : AddLECancellable c)
    (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < c ↔ a - c < b := by
  rw [hb.tsub_lt_iff_left h₁, hc.tsub_lt_iff_right h₂]

Cancellable Subtraction Inequality: $a - b < c \leftrightarrow a - c < b$

Informal description

Let $a$, $b$, and $c$ be elements in a canonically ordered monoid, and suppose $b$ and $c$ are additively left cancellable (i.e., $b + x \leq b + y$ implies $x \leq y$ and similarly for $c$). If $b \leq a$ and $c \leq a$, then $a - b < c$ if and only if $a - c < b$.

AddLECancellable.le_tsub_iff_le_tsub theorem

(ha : AddLECancellable a) (hc : AddLECancellable c) (h₁ : a ≤ b) (h₂ : c ≤ b) : a ≤ b - c ↔ c ≤ b - a

Full source

protected theorem le_tsub_iff_le_tsub (ha : AddLECancellable a) (hc : AddLECancellable c)
    (h₁ : a ≤ b) (h₂ : c ≤ b) : a ≤ b - c ↔ c ≤ b - a := by
  rw [ha.le_tsub_iff_left h₁, hc.le_tsub_iff_right h₂]

Cancellable Subtraction Inequality: $a \leq b - c \leftrightarrow c \leq b - a$

Informal description

Let $a$, $b$, and $c$ be elements in a canonically ordered monoid, and suppose $a$ and $c$ are additively left cancellable (i.e., $a + x \leq a + y$ implies $x \leq y$ and similarly for $c$). If $a \leq b$ and $c \leq b$, then $a \leq b - c$ if and only if $c \leq b - a$.

AddLECancellable.lt_tsub_iff_right_of_le theorem

(hc : AddLECancellable c) (h : c ≤ b) : a < b - c ↔ a + c < b

Full source

protected theorem lt_tsub_iff_right_of_le (hc : AddLECancellable c) (h : c ≤ b) :
    a < b - c ↔ a + c < b := by
  refine ⟨fun h' => (add_le_of_le_tsub_right_of_le h h'.le).lt_of_ne ?_, hc.lt_tsub_of_add_lt_right⟩
  rintro rfl
  exact h'.ne' hc.add_tsub_cancel_right

Strict Inequality via Right Subtraction under Cancellability: $a < b - c \leftrightarrow a + c < b$

Informal description

Let $\alpha$ be a canonically ordered monoid. For any elements $a, b, c \in \alpha$ such that $c$ is additively left cancellable and $c \leq b$, we have $a < b - c$ if and only if $a + c < b$.

AddLECancellable.lt_tsub_iff_left_of_le theorem

(hc : AddLECancellable c) (h : c ≤ b) : a < b - c ↔ c + a < b

Full source

protected theorem lt_tsub_iff_left_of_le (hc : AddLECancellable c) (h : c ≤ b) :
    a < b - c ↔ c + a < b := by
  rw [add_comm]
  exact hc.lt_tsub_iff_right_of_le h

Strict Inequality via Left Subtraction under Cancellability: $a < b - c \leftrightarrow c + a < b$

Informal description

Let $\alpha$ be a canonically ordered monoid. For any elements $a, b, c \in \alpha$ such that $c$ is additively left cancellable and $c \leq b$, we have $a < b - c$ if and only if $c + a < b$.

AddLECancellable.tsub_inj_right theorem

(hab : AddLECancellable (a - b)) (h₁ : b ≤ a) (h₂ : c ≤ a) (h₃ : a - b = a - c) : b = c

Full source

protected theorem tsub_inj_right (hab : AddLECancellable (a - b)) (h₁ : b ≤ a) (h₂ : c ≤ a)
    (h₃ : a - b = a - c) : b = c := by
  rw [← hab.inj]
  rw [tsub_add_cancel_of_le h₁, h₃, tsub_add_cancel_of_le h₂]

Injective Right Subtraction under Cancellability and Order Conditions

Informal description

Let $\alpha$ be a canonically ordered monoid. For any elements $a, b, c \in \alpha$, if $a - b$ is additively left cancellable, $b \leq a$, $c \leq a$, and $a - b = a - c$, then $b = c$.

AddLECancellable.lt_of_tsub_lt_tsub_left_of_le theorem

[AddLeftReflectLT α] (hb : AddLECancellable b) (hca : c ≤ a) (h : a - b < a - c) : c < b

Full source

protected theorem lt_of_tsub_lt_tsub_left_of_le [AddLeftReflectLT α]
    (hb : AddLECancellable b) (hca : c ≤ a) (h : a - b < a - c) : c < b := by
  conv_lhs at h => rw [← tsub_add_cancel_of_le hca]
  exact lt_of_add_lt_add_left (hb.lt_add_of_tsub_lt_right h)

Strict Order Reflection via Left Subtraction: $a - b < a - c \Rightarrow c < b$ under cancellability and order conditions

Informal description

Let $\alpha$ be a canonically ordered monoid where addition reflects the strict order on the left. For any elements $a, b, c \in \alpha$, if $b$ is additively left cancellable, $c \leq a$, and $a - b < a - c$, then $c < b$.

AddLECancellable.tsub_lt_tsub_left_of_le theorem

(hab : AddLECancellable (a - b)) (h₁ : b ≤ a) (h : c < b) : a - b < a - c

Full source

protected theorem tsub_lt_tsub_left_of_le (hab : AddLECancellable (a - b)) (h₁ : b ≤ a)
    (h : c < b) : a - b < a - c :=
  (tsub_le_tsub_left h.le _).lt_of_ne fun h' => h.ne' <| hab.tsub_inj_right h₁ (h.le.trans h₁) h'

Strict Inequality Preservation under Left Subtraction for Cancellable Elements

Informal description

Let $\alpha$ be a canonically ordered monoid. For any elements $a, b, c \in \alpha$, if $a - b$ is additively left cancellable, $b \leq a$, and $c < b$, then $a - b < a - c$.

AddLECancellable.tsub_lt_tsub_right_of_le theorem

(hc : AddLECancellable c) (h : c ≤ a) (h2 : a < b) : a - c < b - c

Full source

protected theorem tsub_lt_tsub_right_of_le (hc : AddLECancellable c) (h : c ≤ a) (h2 : a < b) :
    a - c < b - c := by
  apply hc.lt_tsub_of_add_lt_left
  rwa [add_tsub_cancel_of_le h]

Right Subtraction Preserves Strict Inequality for Additively Left Cancellable Elements

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $c$ is additively left cancellable, $c \leq a$, and $a < b$, then $a - c < b - c$.

AddLECancellable.tsub_lt_tsub_iff_left_of_le_of_le theorem

 [AddLeftReflectLT α] (hb : AddLECancellable b) (hab : AddLECancellable (a - b)) (h₁ : b ≤ a) (h₂ : c ≤ a) :
  a - b < a - c ↔ c < b

Full source

protected theorem tsub_lt_tsub_iff_left_of_le_of_le [AddLeftReflectLT α]
    (hb : AddLECancellable b) (hab : AddLECancellable (a - b)) (h₁ : b ≤ a) (h₂ : c ≤ a) :
    a - b < a - c ↔ c < b :=
  ⟨hb.lt_of_tsub_lt_tsub_left_of_le h₂, hab.tsub_lt_tsub_left_of_le h₁⟩

Strict Inequality Equivalence via Left Subtraction: $a - b < a - c \leftrightarrow c < b$ under cancellability and order conditions

Informal description

Let $\alpha$ be a canonically ordered monoid where addition reflects the strict order on the left. For any elements $a, b, c \in \alpha$, if $b$ and $a - b$ are additively left cancellable, $b \leq a$, and $c \leq a$, then $a - b < a - c$ if and only if $c < b$.

AddLECancellable.add_add_tsub_cancel theorem

(hc : AddLECancellable c) (hcb : c ≤ b) : a + c + (b - c) = a + b

Full source

@[simp]
protected lemma add_add_tsub_cancel (hc : AddLECancellable c) (hcb : c ≤ b) :
    a + c + (b - c) = a + b := by
  rw [← hc.add_tsub_assoc_of_le hcb, add_right_comm, hc.add_tsub_cancel_right]

Addition-Subtraction Cancellation: $(a + c) + (b - c) = a + b$ under cancellability condition

Informal description

Let $a$, $b$, and $c$ be elements of a canonically ordered monoid. If $c$ is additively left cancellable and $c \leq b$, then $(a + c) + (b - c) = a + b$.

AddLECancellable.add_tsub_tsub_cancel theorem

(hac : AddLECancellable (a - c)) (h : c ≤ a) : a + b - (a - c) = b + c

Full source

@[simp]
protected theorem add_tsub_tsub_cancel (hac : AddLECancellable (a - c)) (h : c ≤ a) :
    a + b - (a - c) = b + c :=
  hac.tsub_eq_of_eq_add <| by rw [add_assoc, add_tsub_cancel_of_le h, add_comm]

Subtraction Cancellation in Ordered Monoid: $(a + b) - (a - c) = b + c$ when $c \leq a$ and $a - c$ is cancellable

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $a - c$ is additively left cancellable and $c \leq a$, then $(a + b) - (a - c) = b + c$.

AddLECancellable.tsub_tsub_cancel_of_le theorem

(hba : AddLECancellable (b - a)) (h : a ≤ b) : b - (b - a) = a

Full source

protected theorem tsub_tsub_cancel_of_le (hba : AddLECancellable (b - a)) (h : a ≤ b) :
    b - (b - a) = a :=
  hba.tsub_eq_of_eq_add (add_tsub_cancel_of_le h).symm

Double Subtraction Cancellation: $b - (b - a) = a$ under cancellability condition

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid, if $a \leq b$ and the subtraction $b - a$ is additively left-cancellable, then $b - (b - a) = a$.

AddLECancellable.tsub_tsub_tsub_cancel_left theorem

(hab : AddLECancellable (a - b)) (h : b ≤ a) : a - c - (a - b) = b - c

Full source

protected theorem tsub_tsub_tsub_cancel_left (hab : AddLECancellable (a - b)) (h : b ≤ a) :
    a - c - (a - b) = b - c := by rw [tsub_right_comm, hab.tsub_tsub_cancel_of_le h]

Left Triple Subtraction Cancellation: $(a - c) - (a - b) = b - c$ under cancellability condition

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $b \leq a$ and the subtraction $a - b$ is additively left-cancellable, then $(a - c) - (a - b) = b - c$.

tsub_eq_iff_eq_add_of_le theorem

(h : b ≤ a) : a - b = c ↔ a = c + b

Full source

theorem tsub_eq_iff_eq_add_of_le (h : b ≤ a) : a - b = c ↔ a = c + b :=
  Contravariant.AddLECancellable.tsub_eq_iff_eq_add_of_le h

Subtraction Equivalence: $a - b = c \leftrightarrow a = c + b$ under $b \leq a$

Informal description

For elements $a$, $b$, and $c$ in a canonically ordered monoid, if $b \leq a$, then the subtraction $a - b$ equals $c$ if and only if $a$ equals $c + b$.

add_tsub_assoc_of_le theorem

(h : c ≤ b) (a : α) : a + b - c = a + (b - c)

Full source

/-- See `add_tsub_le_assoc` for an inequality. -/
theorem add_tsub_assoc_of_le (h : c ≤ b) (a : α) : a + b - c = a + (b - c) :=
  Contravariant.AddLECancellable.add_tsub_assoc_of_le h a

Associativity of Addition and Subtraction: $(a + b) - c = a + (b - c)$ under $c \leq b$

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $c \leq b$, then $(a + b) - c = a + (b - c)$.

tsub_add_eq_add_tsub theorem

(h : b ≤ a) : a - b + c = a + c - b

Full source

theorem tsub_add_eq_add_tsub (h : b ≤ a) : a - b + c = a + c - b :=
  Contravariant.AddLECancellable.tsub_add_eq_add_tsub h

Subtraction-Add Commutativity: $(a - b) + c = (a + c) - b$ under $b \leq a$

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $b \leq a$, then $(a - b) + c = (a + c) - b$.

tsub_tsub_assoc theorem

(h₁ : b ≤ a) (h₂ : c ≤ b) : a - (b - c) = a - b + c

Full source

theorem tsub_tsub_assoc (h₁ : b ≤ a) (h₂ : c ≤ b) : a - (b - c) = a - b + c :=
  Contravariant.AddLECancellable.tsub_tsub_assoc h₁ h₂

Associativity of Double Subtraction: $a - (b - c) = a - b + c$ under $b \leq a$ and $c \leq b$

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $b \leq a$ and $c \leq b$, then $a - (b - c) = a - b + c$.

tsub_add_tsub_comm theorem

(hba : b ≤ a) (hdc : d ≤ c) : a - b + (c - d) = a + c - (b + d)

Full source

theorem tsub_add_tsub_comm (hba : b ≤ a) (hdc : d ≤ c) : a - b + (c - d) = a + c - (b + d) :=
  Contravariant.AddLECancellable.tsub_add_tsub_comm Contravariant.AddLECancellable hba hdc

Subtraction-Add Commutativity: $(a - b) + (c - d) = (a + c) - (b + d)$ under $b \leq a$ and $d \leq c$

Informal description

For any elements $a$, $b$, $c$, and $d$ in a canonically ordered monoid, if $b \leq a$ and $d \leq c$, then $(a - b) + (c - d) = (a + c) - (b + d)$.

le_tsub_iff_left theorem

(h : a ≤ c) : b ≤ c - a ↔ a + b ≤ c

Full source

theorem le_tsub_iff_left (h : a ≤ c) : b ≤ c - a ↔ a + b ≤ c :=
  Contravariant.AddLECancellable.le_tsub_iff_left h

Subtraction Inequality: $b \leq c - a \leftrightarrow a + b \leq c$

Informal description

For elements $a$, $b$, and $c$ in a canonically ordered monoid, if $a \leq c$, then $b \leq c - a$ if and only if $a + b \leq c$.

le_tsub_iff_right theorem

(h : a ≤ c) : b ≤ c - a ↔ b + a ≤ c

Full source

theorem le_tsub_iff_right (h : a ≤ c) : b ≤ c - a ↔ b + a ≤ c :=
  Contravariant.AddLECancellable.le_tsub_iff_right h

Subtraction Inequality: $b \leq c - a \leftrightarrow b + a \leq c$

Informal description

For elements $a$, $b$, and $c$ in a canonically ordered monoid, if $a \leq c$, then $b \leq c - a$ if and only if $b + a \leq c$.

tsub_lt_iff_left theorem

(hbc : b ≤ a) : a - b < c ↔ a < b + c

Full source

theorem tsub_lt_iff_left (hbc : b ≤ a) : a - b < c ↔ a < b + c :=
  Contravariant.AddLECancellable.tsub_lt_iff_left hbc

Subtraction Inequality: $a - b < c \leftrightarrow a < b + c$

Informal description

For elements $a$, $b$, and $c$ in a canonically ordered monoid, if $b \leq a$, then $a - b < c$ if and only if $a < b + c$.

tsub_lt_iff_right theorem

(hbc : b ≤ a) : a - b < c ↔ a < c + b

Full source

theorem tsub_lt_iff_right (hbc : b ≤ a) : a - b < c ↔ a < c + b :=
  Contravariant.AddLECancellable.tsub_lt_iff_right hbc

Subtraction Inequality: $a - b < c \leftrightarrow a < c + b$

Informal description

For elements $a$, $b$, and $c$ in a canonically ordered monoid, if $b \leq a$, then $a - b < c$ if and only if $a < c + b$.

tsub_lt_iff_tsub_lt theorem

(h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < c ↔ a - c < b

Full source

theorem tsub_lt_iff_tsub_lt (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < c ↔ a - c < b :=
  Contravariant.AddLECancellable.tsub_lt_iff_tsub_lt Contravariant.AddLECancellable h₁ h₂

Subtraction Inequality Swap: $a - b < c \leftrightarrow a - c < b$ under $b, c \leq a$

Informal description

For elements $a$, $b$, and $c$ in a canonically ordered monoid, if $b \leq a$ and $c \leq a$, then $a - b < c$ if and only if $a - c < b$.

le_tsub_iff_le_tsub theorem

(h₁ : a ≤ b) (h₂ : c ≤ b) : a ≤ b - c ↔ c ≤ b - a

Full source

theorem le_tsub_iff_le_tsub (h₁ : a ≤ b) (h₂ : c ≤ b) : a ≤ b - c ↔ c ≤ b - a :=
  Contravariant.AddLECancellable.le_tsub_iff_le_tsub Contravariant.AddLECancellable h₁ h₂

Subtraction Order Equivalence: $a \leq b - c \leftrightarrow c \leq b - a$

Informal description

Let $a$, $b$, and $c$ be elements in a canonically ordered monoid such that $a \leq b$ and $c \leq b$. Then $a \leq b - c$ if and only if $c \leq b - a$.

lt_tsub_iff_right_of_le theorem

(h : c ≤ b) : a < b - c ↔ a + c < b

Full source

/-- See `lt_tsub_iff_right` for a stronger statement in a linear order. -/
theorem lt_tsub_iff_right_of_le (h : c ≤ b) : a < b - c ↔ a + c < b :=
  Contravariant.AddLECancellable.lt_tsub_iff_right_of_le h

Strict inequality via right subtraction: $a < b - c \leftrightarrow a + c < b$ under $c \leq b$

Informal description

Let $\alpha$ be a canonically ordered monoid. For any elements $a, b, c \in \alpha$ such that $c \leq b$, we have $a < b - c$ if and only if $a + c < b$.

lt_tsub_iff_left_of_le theorem

(h : c ≤ b) : a < b - c ↔ c + a < b

Full source

/-- See `lt_tsub_iff_left` for a stronger statement in a linear order. -/
theorem lt_tsub_iff_left_of_le (h : c ≤ b) : a < b - c ↔ c + a < b :=
  Contravariant.AddLECancellable.lt_tsub_iff_left_of_le h

Strict inequality via left subtraction: $a < b - c \leftrightarrow c + a < b$ under $c \leq b$

Informal description

Let $\alpha$ be a canonically ordered monoid. For any elements $a, b, c \in \alpha$ such that $c \leq b$, we have $a < b - c$ if and only if $c + a < b$.

lt_of_tsub_lt_tsub_left_of_le theorem

[AddLeftReflectLT α] (hca : c ≤ a) (h : a - b < a - c) : c < b

Full source

/-- See `lt_of_tsub_lt_tsub_left` for a stronger statement in a linear order. -/
theorem lt_of_tsub_lt_tsub_left_of_le [AddLeftReflectLT α] (hca : c ≤ a)
    (h : a - b < a - c) : c < b :=
  Contravariant.AddLECancellable.lt_of_tsub_lt_tsub_left_of_le hca h

Strict Order Reflection via Left Subtraction: $a - b < a - c \Rightarrow c < b$ under order condition

Informal description

Let $\alpha$ be a canonically ordered monoid where addition reflects the strict order on the left. For any elements $a, b, c \in \alpha$, if $c \leq a$ and $a - b < a - c$, then $c < b$.

tsub_lt_tsub_left_of_le theorem

: b ≤ a → c < b → a - b < a - c

Full source

theorem tsub_lt_tsub_left_of_le : b ≤ a → c < b → a - b < a - c :=
  Contravariant.AddLECancellable.tsub_lt_tsub_left_of_le

Left Subtraction Preserves Strict Inequality under Order Conditions

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $b \leq a$ and $c < b$, then $a - b < a - c$.

tsub_lt_tsub_right_of_le theorem

(h : c ≤ a) (h2 : a < b) : a - c < b - c

Full source

theorem tsub_lt_tsub_right_of_le (h : c ≤ a) (h2 : a < b) : a - c < b - c :=
  Contravariant.AddLECancellable.tsub_lt_tsub_right_of_le h h2

Right Subtraction Preserves Strict Inequality under Order Conditions

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $c \leq a$ and $a < b$, then $a - c < b - c$.

tsub_inj_right theorem

(h₁ : b ≤ a) (h₂ : c ≤ a) (h₃ : a - b = a - c) : b = c

Full source

theorem tsub_inj_right (h₁ : b ≤ a) (h₂ : c ≤ a) (h₃ : a - b = a - c) : b = c :=
  Contravariant.AddLECancellable.tsub_inj_right h₁ h₂ h₃

Right Subtraction is Injective under Order Conditions

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $b \leq a$, $c \leq a$, and $a - b = a - c$, then $b = c$.

tsub_lt_tsub_iff_left_of_le_of_le theorem

[AddLeftReflectLT α] (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < a - c ↔ c < b

Full source

/-- See `tsub_lt_tsub_iff_left_of_le` for a stronger statement in a linear order. -/
theorem tsub_lt_tsub_iff_left_of_le_of_le [AddLeftReflectLT α] (h₁ : b ≤ a)
    (h₂ : c ≤ a) : a - b < a - c ↔ c < b :=
  Contravariant.AddLECancellable.tsub_lt_tsub_iff_left_of_le_of_le Contravariant.AddLECancellable h₁
    h₂

Strict Inequality Equivalence via Left Subtraction: $a - b < a - c \leftrightarrow c < b$ under order conditions

Informal description

Let $\alpha$ be a canonically ordered monoid where addition reflects the strict order on the left. For any elements $a, b, c \in \alpha$ such that $b \leq a$ and $c \leq a$, we have $a - b < a - c$ if and only if $c < b$.

add_add_tsub_cancel theorem

(hcb : c ≤ b) : a + c + (b - c) = a + b

Full source

@[simp]
lemma add_add_tsub_cancel (hcb : c ≤ b) : a + c + (b - c) = a + b :=
  Contravariant.AddLECancellable.add_add_tsub_cancel hcb

Addition-Subtraction Cancellation: $(a + c) + (b - c) = a + b$ when $c \leq b$

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $c \leq b$, then $(a + c) + (b - c) = a + b$.

add_tsub_tsub_cancel theorem

(h : c ≤ a) : a + b - (a - c) = b + c

Full source

@[simp]
theorem add_tsub_tsub_cancel (h : c ≤ a) : a + b - (a - c) = b + c :=
  Contravariant.AddLECancellable.add_tsub_tsub_cancel h

Subtraction Cancellation: $(a + b) - (a - c) = b + c$ when $c \leq a$

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $c \leq a$, then $(a + b) - (a - c) = b + c$.

tsub_tsub_cancel_of_le theorem

(h : a ≤ b) : b - (b - a) = a

Full source

/-- See `tsub_tsub_le` for an inequality. -/
theorem tsub_tsub_cancel_of_le (h : a ≤ b) : b - (b - a) = a :=
  Contravariant.AddLECancellable.tsub_tsub_cancel_of_le h

Double Subtraction Cancellation: $b - (b - a) = a$ when $a \leq b$

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid, if $a \leq b$, then $b - (b - a) = a$.

tsub_tsub_tsub_cancel_left theorem

(h : b ≤ a) : a - c - (a - b) = b - c

Full source

theorem tsub_tsub_tsub_cancel_left (h : b ≤ a) : a - c - (a - b) = b - c :=
  Contravariant.AddLECancellable.tsub_tsub_tsub_cancel_left h

Left Triple Subtraction Cancellation: $(a - c) - (a - b) = b - c$ under $b \leq a$

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $b \leq a$, then $(a - c) - (a - b) = b - c$.

tsub_tsub_eq_add_tsub_of_le theorem

(h : c ≤ b) : a - (b - c) = a + c - b

Full source

/-- The `tsub` version of `sub_sub_eq_add_sub`. -/
theorem tsub_tsub_eq_add_tsub_of_le
    (h : c ≤ b) : a - (b - c) = a + c - b := by
  obtain ⟨d, rfl⟩ := exists_add_of_le h
  rw [add_tsub_cancel_left c, add_comm a c, add_tsub_add_eq_tsub_left]

Subtraction Identity: $a - (b - c) = a + c - b$ when $c \leq b$

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered monoid, if $c \leq b$, then $a - (b - c) = a + c - b$.