lt_add_of_sub_lt_left — Mathlib

English

If a ≠ ∞ or b ≠ ∞ and a − b < c, then a < b + c.

Русский

Если a ≠ ∞ или b ≠ ∞ и a − b < c, то a < b + c.

LaTeX

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

Lean4

protected theorem lt_add_of_sub_lt_left (h : a ≠ ∞ ∨ b ≠ ∞) : a - b < c → a < b + c :=
  by
  obtain rfl | hb := eq_or_ne b ∞
  · rw [top_add, lt_top_iff_ne_top]
    exact fun _ => h.resolve_right (Classical.not_not.2 rfl)
  · exact (cancel_of_ne hb).lt_add_of_tsub_lt_left

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