sub_lt_iff — Mathlib

English

For nondegenerate bounds, c - b < a ↔ c < a + b.

Русский

При ненулевых ограничениях c - b < a ↔ c < a + b.

LaTeX

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

Lean4

theorem sub_lt_iff {a b c : EReal} (h₁ : b ≠ ⊥ ∨ c ≠ ⊥) (h₂ : b ≠ ⊤ ∨ c ≠ ⊤) : c - b < a ↔ c < a + b :=
  lt_iff_lt_of_le_iff_le (le_sub_iff_add_le h₁ h₂)

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