sub_le_iff_le_add — Mathlib

English

For all a,b,c in EReal, if certain bounds hold, then a - b ≤ c ↔ a ≤ c + b.

Русский

Для всех a,b,c в EReal при соблюдении условий ограничений верно: a − b ≤ c ⇔ a ≤ c + b.

LaTeX

$$$\forall a,b,c \in \mathrm{EReal},\ (b \neq \bot \lor c \neq \top) \land (b \neq \top \lor c \neq \bot) \Rightarrow (a - b \le c \iff a \le c + b)$$$

Lean4

theorem sub_le_iff_le_add {a b c : EReal} (h₁ : b ≠ ⊥ ∨ c ≠ ⊤) (h₂ : b ≠ ⊤ ∨ c ≠ ⊥) : a - b ≤ c ↔ a ≤ c + b :=
  by
  suffices a + (-b) ≤ c ↔ a ≤ c - (-b) by simpa [sub_eq_add_neg]
  refine (le_sub_iff_add_le ?_ ?_).symm <;> simpa

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