le_tsub_iff_le_tsub — Mathlib

English

For a and c cancellable on the left and a ≤ b, c ≤ b, we have a ≤ b − c iff c ≤ b − a.

Русский

При левой канселируемости a и c и a ≤ b, c ≤ b имеем a ≤ b − c ⇔ c ≤ b − a.

LaTeX

$$$ \forall a,b,c \in \alpha,\; AddLECancellable(a) \land AddLECancellable(c) \land a \le b \land c \le b \Rightarrow a \le b - c \iff c \le b - a $$$

Lean4

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₂]

Похожие утверждения