Mathlib.Algebra.Order.Sub.Basic

add_tsub_cancel_iff_le theorem

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

Full source

theorem add_tsub_cancel_iff_le : a + (b - a) = b ↔ a ≤ b :=
  ⟨fun h => le_iff_exists_add.mpr ⟨b - a, h.symm⟩, add_tsub_cancel_of_le⟩

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

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid with subtraction, the equation $a + (b - a) = b$ holds if and only if $a \leq b$.

tsub_add_cancel_iff_le theorem

: b - a + a = b ↔ a ≤ b

Full source

theorem tsub_add_cancel_iff_le : b - a + a = b ↔ a ≤ b := by
  rw [add_comm]
  exact add_tsub_cancel_iff_le

Subtraction-Add Cancellation: $(b - a) + a = b \leftrightarrow a \leq b$

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid with subtraction, the equation $(b - a) + a = b$ holds if and only if $a \leq b$.

tsub_eq_zero_iff_le theorem

: a - b = 0 ↔ a ≤ b

Full source

theorem tsub_eq_zero_iff_le : a - b = 0 ↔ a ≤ b := by
  rw [← nonpos_iff_eq_zero, tsub_le_iff_left, add_zero]

Difference Equals Zero iff Ordering Holds: $a - b = 0 \leftrightarrow a \leq b$

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid with subtraction, the difference $a - b$ equals zero if and only if $a \leq b$.

tsub_self theorem

(a : α) : a - a = 0

Full source

@[simp]
theorem tsub_self (a : α) : a - a = 0 :=
  tsub_eq_zero_of_le le_rfl

Self-Subtraction Yields Zero: $a - a = 0$

Informal description

For any element $a$ in a canonically ordered monoid with subtraction, the difference $a - a$ equals zero.

tsub_le_self theorem

: a - b ≤ a

Full source

theorem tsub_le_self : a - b ≤ a :=
  tsub_le_iff_left.mpr <| le_add_left le_rfl

Subtraction is Bounded Above: $a - b \leq a$

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid with subtraction, the difference $a - b$ is less than or equal to $a$.

zero_tsub theorem

(a : α) : 0 - a = 0

Full source

@[simp]
theorem zero_tsub (a : α) : 0 - a = 0 :=
  tsub_eq_zero_of_le <| zero_le a

Subtraction from Zero: $0 - a = 0$

Informal description

For any element $a$ in a canonically ordered monoid with subtraction, the difference $0 - a$ equals $0$.

tsub_self_add theorem

(a b : α) : a - (a + b) = 0

Full source

theorem tsub_self_add (a b : α) : a - (a + b) = 0 :=
  tsub_eq_zero_of_le <| self_le_add_right _ _

Subtraction of Self-Plus-Element: $a - (a + b) = 0$

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid with subtraction, the difference $a - (a + b)$ equals zero, i.e., $a - (a + b) = 0$.

tsub_pos_iff_not_le theorem

: 0 < a - b ↔ ¬a ≤ b

Full source

theorem tsub_pos_iff_not_le : 0 < a - b ↔ ¬a ≤ b := by
  rw [pos_iff_ne_zero, Ne, tsub_eq_zero_iff_le]

Positivity of Difference Characterizes Non-Ordering: $0 < a - b \leftrightarrow \neg (a \leq b)$

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid with subtraction, the difference $a - b$ is positive (i.e., $0 < a - b$) if and only if $a$ is not less than or equal to $b$ (i.e., $\neg (a \leq b)$).

tsub_pos_of_lt theorem

(h : a < b) : 0 < b - a

Full source

theorem tsub_pos_of_lt (h : a < b) : 0 < b - a :=
  tsub_pos_iff_not_le.mpr h.not_le

Positivity of Difference under Strict Inequality: $a < b \Rightarrow 0 < b - a$

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid with subtraction, if $a < b$, then the difference $b - a$ is positive, i.e., $0 < b - a$.

tsub_lt_of_lt theorem

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

Full source

theorem tsub_lt_of_lt (h : a < b) : a - c < b :=
  lt_of_le_of_lt tsub_le_self h

Subtraction Preserves Strict Inequality: $a < b \Rightarrow a - c < b$

Informal description

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

AddLECancellable.tsub_le_tsub_iff_left theorem

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

Full source

protected theorem tsub_le_tsub_iff_left (ha : AddLECancellable a) (hc : AddLECancellable c)
    (h : c ≤ a) : a - b ≤ a - c ↔ c ≤ b := by
  refine ⟨?_, fun h => tsub_le_tsub_left h a⟩
  rw [tsub_le_iff_left, ← hc.add_tsub_assoc_of_le h, hc.le_tsub_iff_right (h.trans le_add_self),
    add_comm b]
  apply ha

Characterization of Subtraction Inequalities in Cancellable Monoids: $a - b \leq a - c \leftrightarrow c \leq b$ under Cancellability Conditions

Informal description

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

AddLECancellable.tsub_right_inj theorem

 (ha : AddLECancellable a) (hb : AddLECancellable b) (hc : AddLECancellable c) (hba : b ≤ a) (hca : c ≤ a) :
  a - b = a - c ↔ b = c

Full source

protected theorem tsub_right_inj (ha : AddLECancellable a) (hb : AddLECancellable b)
    (hc : AddLECancellable c) (hba : b ≤ a) (hca : c ≤ a) : a - b = a - c ↔ b = c := by
  simp_rw [le_antisymm_iff, ha.tsub_le_tsub_iff_left hb hba, ha.tsub_le_tsub_iff_left hc hca,
    and_comm]

Right Subtraction Cancellation in Cancellable Monoids: $a - b = a - c \leftrightarrow b = c$ under Cancellability Conditions

Informal description

Let $a$, $b$, and $c$ be elements of a canonically ordered monoid with subtraction, where $a$, $b$, and $c$ are additively left cancellable (i.e., $a + x \leq a + y$ implies $x \leq y$, and similarly for $b$ and $c$). If $b \leq a$ and $c \leq a$, then the equality $a - b = a - c$ holds if and only if $b = c$.

tsub_le_tsub_iff_left theorem

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

Full source

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

Characterization of Subtraction Inequalities: $a - b \leq a - c \leftrightarrow c \leq b$ under $c \leq a$

Informal description

Let $\alpha$ be a canonically ordered monoid with ordered subtraction. For any elements $a, b, c \in \alpha$ such that $c \leq a$, the inequality $a - b \leq a - c$ holds if and only if $c \leq b$.

tsub_right_inj theorem

(hba : b ≤ a) (hca : c ≤ a) : a - b = a - c ↔ b = c

Full source

theorem tsub_right_inj (hba : b ≤ a) (hca : c ≤ a) : a - b = a - c ↔ b = c :=
  Contravariant.AddLECancellable.tsub_right_inj Contravariant.AddLECancellable
    Contravariant.AddLECancellable hba hca

Right Subtraction Cancellation: $a - b = a - c \leftrightarrow b = c$ under $b, c \leq a$

Informal description

Let $\alpha$ be a canonically ordered monoid with ordered subtraction. For any elements $a, b, c \in \alpha$ such that $b \leq a$ and $c \leq a$, the equality $a - b = a - c$ holds if and only if $b = c$.

CanonicallyOrderedAddCommMonoid.toAddCancelCommMonoid abbrev

: AddCancelCommMonoid α

Full source

/-- 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]. -/
abbrev CanonicallyOrderedAddCommMonoid.toAddCancelCommMonoid : AddCancelCommMonoid α :=
  { (by infer_instance : AddCommMonoid α) with
    add_left_cancel := fun a b c h => by
      simpa only [add_tsub_cancel_left] using congr_arg (fun x => x - a) h }

Cancellativity in Canonically Ordered Additive Commutative Monoids with Ordered Subtraction

Informal description

A canonically ordered additive commutative monoid with ordered subtraction and order-reflecting addition is cancellative. That is, for any elements $a, b, c$ in the monoid, if $a + b = a + c$, then $b = c$.

tsub_pos_iff_lt theorem

: 0 < a - b ↔ b < a

Full source

@[simp]
theorem tsub_pos_iff_lt : 0 < a - b ↔ b < a := by rw [tsub_pos_iff_not_le, not_le]

Positivity of Difference Characterizes Strict Ordering: $0 < a - b \leftrightarrow b < a$

Informal description

For any elements $a$ and $b$ in a canonically ordered additive monoid with subtraction, the difference $a - b$ is positive (i.e., $0 < a - b$) if and only if $b$ is strictly less than $a$ (i.e., $b < a$).

tsub_eq_tsub_min theorem

(a b : α) : a - b = a - min a b

Full source

theorem tsub_eq_tsub_min (a b : α) : a - b = a - min a b := by
  rcases le_total a b with h | h
  · rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]
  · rw [min_eq_right h]

Subtraction Equals Subtraction of Minimum: $a - b = a - \min(a, b)$

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid with subtraction, the difference $a - b$ equals the difference $a - \min(a, b)$.

AddLECancellable.lt_tsub_iff_right theorem

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

Full source

protected theorem lt_tsub_iff_right (hc : AddLECancellable c) : a < b - c ↔ a + c < b :=
  ⟨lt_imp_lt_of_le_imp_le tsub_le_iff_right.mpr, hc.lt_tsub_of_add_lt_right⟩

Characterization of Strict Subtraction Inequality via Cancellable Addition: $a < b - c \leftrightarrow a + c < b$

Informal description

Let $\alpha$ be a type with a partial order $\leq$, addition $+$, and subtraction $-$, satisfying the `OrderedSub` property. For an additively left cancellable element $c \in \alpha$ (i.e., $x + c \leq y + c$ implies $x \leq y$), the inequality $a < b - c$ holds if and only if $a + c < b$.

AddLECancellable.lt_tsub_iff_left theorem

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

Full source

protected theorem lt_tsub_iff_left (hc : AddLECancellable c) : a < b - c ↔ c + a < b :=
  ⟨lt_imp_lt_of_le_imp_le tsub_le_iff_left.mpr, hc.lt_tsub_of_add_lt_left⟩

Characterization of Strict Subtraction Inequality via Left Cancellable Addition: $a < b - c \leftrightarrow c + a < b$

Informal description

Let $\alpha$ be a type with a partial order $\leq$, addition $+$, and subtraction $-$, satisfying the `OrderedSub` property. For an additively left cancellable element $c \in \alpha$ (i.e., $x + c \leq y + c$ implies $x \leq y$), the inequality $a < b - c$ holds if and only if $c + a < b$.

AddLECancellable.tsub_lt_tsub_iff_right theorem

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

Full source

protected theorem tsub_lt_tsub_iff_right (hc : AddLECancellable c) (h : c ≤ a) :
    a - c < b - c ↔ a < b := by rw [hc.lt_tsub_iff_left, add_tsub_cancel_of_le h]

Subtraction Preserves Strict Inequality for Cancellable Elements: $a - c < b - c \leftrightarrow a < b$ when $c \leq a$

Informal description

Let $\alpha$ be a canonically ordered monoid with subtraction, and let $c \in \alpha$ be an additively left cancellable element (i.e., $x + c \leq y + c$ implies $x \leq y$). For any elements $a, b \in \alpha$ such that $c \leq a$, the inequality $a - c < b - c$ holds if and only if $a < b$.

AddLECancellable.tsub_lt_self theorem

(ha : AddLECancellable a) (h₁ : 0 < a) (h₂ : 0 < b) : a - b < a

Full source

protected theorem tsub_lt_self (ha : AddLECancellable a) (h₁ : 0 < a) (h₂ : 0 < b) : a - b < a := by
  refine tsub_le_self.lt_of_ne fun h => ?_
  rw [← h, tsub_pos_iff_lt] at h₁
  exact h₂.not_le (ha.add_le_iff_nonpos_left.1 <| add_le_of_le_tsub_left_of_le h₁.le h.ge)

Strict Subtraction Inequality for Cancellable Elements: $a - b < a$ when $a, b > 0$

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid where $a$ is additively left cancellable (i.e., $a + x \leq a + y$ implies $x \leq y$), if $0 < a$ and $0 < b$, then $a - b < a$.

AddLECancellable.tsub_lt_self_iff theorem

(ha : AddLECancellable a) : a - b < a ↔ 0 < a ∧ 0 < b

Full source

protected theorem tsub_lt_self_iff (ha : AddLECancellable a) : a - b < a ↔ 0 < a ∧ 0 < b := by
  refine
    ⟨fun h => ⟨(zero_le _).trans_lt h, (zero_le b).lt_of_ne ?_⟩, fun h => ha.tsub_lt_self h.1 h.2⟩
  rintro rfl
  rw [tsub_zero] at h
  exact h.false

Characterization of Strict Subtraction Inequality: $a - b < a \leftrightarrow (a > 0 \land b > 0)$ for Cancellable Elements

Informal description

Let $a$ be an additively left cancellable element in a canonically ordered monoid. Then the inequality $a - b < a$ holds if and only if both $a > 0$ and $b > 0$.

AddLECancellable.tsub_lt_tsub_iff_left_of_le theorem

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

Full source

/-- See `lt_tsub_iff_left_of_le_of_le` for a weaker statement in a partial order. -/
protected theorem tsub_lt_tsub_iff_left_of_le (ha : AddLECancellable a) (hb : AddLECancellable b)
    (h : b ≤ a) : a - b < a - c ↔ c < b :=
  lt_iff_lt_of_le_iff_le <| ha.tsub_le_tsub_iff_left hb h

Strict Subtraction Inequality Characterization: $a - b < a - c \leftrightarrow c < b$ under Cancellability Conditions

Informal description

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

tsub_lt_tsub_iff_right theorem

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

Full source

/-- This lemma also holds for `ENNReal`, but we need a different proof for that. -/
theorem tsub_lt_tsub_iff_right (h : c ≤ a) : a - c < b - c ↔ a < b :=
  Contravariant.AddLECancellable.tsub_lt_tsub_iff_right h

Subtraction Preserves Strict Inequality: $a - c < b - c \leftrightarrow a < b$ when $c \leq a$

Informal description

Let $\alpha$ be a canonically ordered monoid with subtraction. For any elements $a, b, c \in \alpha$ such that $c \leq a$, the inequality $a - c < b - c$ holds if and only if $a < b$.

tsub_lt_self theorem

: 0 < a → 0 < b → a - b < a

Full source

theorem tsub_lt_self : 0 < a → 0 < b → a - b < a :=
  Contravariant.AddLECancellable.tsub_lt_self

Strict inequality for subtraction: $a - b < a$ when $a, b > 0$

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid with subtraction, if $0 < a$ and $0 < b$, then $a - b < a$.

tsub_lt_self_iff theorem

: a - b < a ↔ 0 < a ∧ 0 < b

Full source

@[simp] theorem tsub_lt_self_iff : a - b < a ↔ 0 < a ∧ 0 < b :=
  Contravariant.AddLECancellable.tsub_lt_self_iff

Characterization of Strict Subtraction Inequality: $a - b < a \leftrightarrow (a > 0 \land b > 0)$

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid with subtraction, the inequality $a - b < a$ holds if and only if both $a > 0$ and $b > 0$.

tsub_lt_tsub_iff_left_of_le theorem

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

Full source

/-- See `lt_tsub_iff_left_of_le_of_le` for a weaker statement in a partial order. -/
theorem tsub_lt_tsub_iff_left_of_le (h : b ≤ a) : a - b < a - c ↔ c < b :=
  Contravariant.AddLECancellable.tsub_lt_tsub_iff_left_of_le Contravariant.AddLECancellable h

Strict Subtraction Inequality: $a - b < a - c \leftrightarrow c < b$ when $b \leq a$

Informal description

Let $a$, $b$, and $c$ be elements of a canonically ordered monoid with subtraction. If $b \leq a$, then the strict inequality $a - b < a - c$ holds if and only if $c < b$.

tsub_tsub_eq_min theorem

(a b : α) : a - (a - b) = min a b

Full source

lemma tsub_tsub_eq_min (a b : α) : a - (a - b) = min a b := by
  rw [tsub_eq_tsub_min _ b, tsub_tsub_cancel_of_le (min_le_left a _)]

Double Subtraction Equals Minimum: $a - (a - b) = \min(a, b)$

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid with subtraction, the double subtraction $a - (a - b)$ equals the minimum of $a$ and $b$, i.e., $a - (a - b) = \min(a, b)$.

tsub_add_eq_max theorem

: a - b + b = max a b

Full source

theorem tsub_add_eq_max : a - b + b = max a b := by
  rcases le_total a b with h | h
  · rw [max_eq_right h, tsub_eq_zero_of_le h, zero_add]
  · rw [max_eq_left h, tsub_add_cancel_of_le h]

Truncated Subtraction-Add Identity: $(a - b) + b = \max(a, b)$

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid with subtraction, the sum of the truncated subtraction $a - b$ and $b$ equals the maximum of $a$ and $b$, i.e., $(a - b) + b = \max(a, b)$.

add_tsub_eq_max theorem

: a + (b - a) = max a b

Full source

theorem add_tsub_eq_max : a + (b - a) = max a b := by rw [add_comm, max_comm, tsub_add_eq_max]

Addition-Truncated Subtraction Identity: $a + (b - a) = \max(a, b)$

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid with subtraction, the sum of $a$ and the truncated subtraction $b - a$ equals the maximum of $a$ and $b$, i.e., $a + (b - a) = \max(a, b)$.

tsub_min theorem

: a - min a b = a - b

Full source

theorem tsub_min : a - min a b = a - b := by
  rcases le_total a b with h | h
  · rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]
  · rw [min_eq_right h]

Truncated Subtraction-Minimum Identity: $a - \min(a, b) = a - b$

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid with subtraction, the truncated subtraction of $a$ and the minimum of $a$ and $b$ equals the truncated subtraction of $a$ and $b$, i.e., $a - \min(a, b) = a - b$.

tsub_add_min theorem

: a - b + min a b = a

Full source

theorem tsub_add_min : a - b + min a b = a := by
  rw [← tsub_min, @tsub_add_cancel_of_le]
  apply min_le_left

Subtraction-Minimum Addition Identity: $(a - b) + \min(a, b) = a$

Informal description

For any elements $a$ and $b$ in a canonically ordered monoid with subtraction, the sum of the truncated subtraction $a - b$ and the minimum of $a$ and $b$ equals $a$, i.e., $(a - b) + \min(a, b) = a$.

Even.tsub theorem

[AddLeftReflectLE α] {m n : α} (hm : Even m) (hn : Even n) : Even (m - n)

Full source

lemma Even.tsub [AddLeftReflectLE α] {m n : α} (hm : Even m) (hn : Even n) :
    Even (m - n) := by
  obtain ⟨a, rfl⟩ := hm
  obtain ⟨b, rfl⟩ := hn
  refine ⟨a - b, ?_⟩
  obtain h | h := le_total a b
  · rw [tsub_eq_zero_of_le h, tsub_eq_zero_of_le (add_le_add h h), add_zero]
  · exact (tsub_add_tsub_comm h h).symm

Evenness is preserved under subtraction in canonically ordered monoids with order-reflecting addition

Informal description

Let $\alpha$ be a canonically ordered monoid where addition reflects the order relation (i.e., $a + b \leq a + c$ implies $b \leq c$). For any elements $m, n \in \alpha$ such that both $m$ and $n$ are even, their difference $m - n$ is also even.