le_sub_iff_add_le_right — Mathlib

English

Let a,b,c ∈ ENNReal with c ≠ ∞ and c ≤ b. Then a ≤ b − c if and only if a + c ≤ b.

Русский

Пусть a, b, c ∈ ℝ≥0∞ с c ≠ ∞ и c ≤ b. Тогда a ≤ b − c тогда и только если a + c ≤ b.

LaTeX

$$$ (a,b,c)\in \mathbb{R}_{\ge 0}^{\infty}\ \text{with}\ c \neq \infty\ \text{and}\ c \le b:\; a \le b - c \iff a + c \le b $$$

Lean4

theorem le_sub_iff_add_le_right (hc : c ≠ ∞) (hcb : c ≤ b) : a ≤ b - c ↔ a + c ≤ b :=
  ⟨fun h ↦ add_le_of_le_tsub_right_of_le hcb h, le_sub_of_add_le_right hc⟩

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