sub_lt_of_sub_lt — Mathlib

English

If c ≤ a, and (a ≠ ∞ ∨ b ≠ ∞), and a − b < c, then a − c < b.

Русский

Если c ≤ a и (a не бесконечность или b не бесконечность), и a − b < c, то a − c < b.

LaTeX

$$$ (c \le a) \land (a \neq \infty \lor b \neq \infty) \land (a - b < c) \Rightarrow a - c < b $$$

Lean4

theorem sub_lt_of_sub_lt (h₂ : c ≤ a) (h₃ : a ≠ ∞ ∨ b ≠ ∞) (h₁ : a - b < c) : a - c < b :=
  ENNReal.sub_lt_of_lt_add h₂ (add_comm c b ▸ ENNReal.lt_add_of_sub_lt_right h₃ h₁)

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