add_le_of_forall_lt — Mathlib

English

If for all a' > a and b' > b we have a' + b' ≤ c, then a + b ≤ c.

Русский

Если для всех a' > a и b' > b выполнено a' + b' ≤ c, то a + b ≤ c.

LaTeX

$$$\forall a,b,c \in \mathrm{EReal},\ (\forall a' > a,\, \forall b' > b,\ a' + b' \le c) \Rightarrow a + b \le c$$$

Lean4

theorem add_le_of_forall_lt {a b c : EReal} (h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c) : a + b ≤ c :=
  by
  refine le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_
  obtain ⟨a', ha', hd⟩ := exists_lt_add_left hd
  obtain ⟨b', hb', hd⟩ := exists_lt_add_right hd
  exact hd.le.trans (h _ ha' _ hb')

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