English
If for all a' > a or b' > b we have c ≤ a' + b', then c ≤ a + b.
Русский
Если для всех a' > a или b' > b верно c ≤ a' + b', то c ≤ a + b.
LaTeX
$$$\forall a,b,c \in \mathrm{EReal},\ (\mathrm{Or} (\mathrm{Ne} a \; \mathrm{bot}) (\mathrm{Ne} b \; \top)) \Rightarrow (\mathrm{Or} (\mathrm{Ne} a \; \top) (\mathrm{Ne} b \; \bot) ) \Rightarrow (\forall a' > a,\, \forall b' > b,\ c \le a' + b') \Rightarrow c \le a + b$$$
Lean4
theorem le_add_of_forall_gt {a b c : EReal} (h₁ : a ≠ ⊥ ∨ b ≠ ⊤) (h₂ : a ≠ ⊤ ∨ b ≠ ⊥)
(h : ∀ a' > a, ∀ b' > b, c ≤ a' + b') : c ≤ a + b :=
by
rw [← neg_le_neg_iff, neg_add h₁ h₂]
refine add_le_of_forall_lt fun a' ha' b' hb' ↦ EReal.le_neg_of_le_neg ?_
rw [neg_add (.inr hb'.ne_top) (.inl ha'.ne_top)]
exact h _ (EReal.lt_neg_of_lt_neg ha') _ (EReal.lt_neg_of_lt_neg hb')
