English
There exists i such that for all j, f_i + g_j ≤ f_k + g_k for some k; then iSup f + iSup g = ⨆ i, f_i + g_i.
Русский
Существует i такой, что для всех j найдется k с f_i + g_j ≤ f_k + g_k; тогда iSup f + iSup g = ⨆ i, f_i + g_i.
LaTeX
$$$\\exists i:\\; f_i + g_j \\le f_k + g_k \\text{ for some } k \\Rightarrow \\bigl(\\sup_i f_i\\bigr) + \\bigl(\\sup_i g_i\\bigr) = \\sup_i (f_i + g_i)$$$
Lean4
theorem iSup_add_iSup (h : ∀ i j, ∃ k, f i + g j ≤ f k + g k) : iSup f + iSup g = ⨆ i, f i + g i :=
by
cases isEmpty_or_nonempty ι
· simp only [iSup_of_empty, bot_eq_zero, zero_add]
· refine le_antisymm ?_ (iSup_le fun a => add_le_add (le_iSup _ _) (le_iSup _ _))
refine iSup_add_iSup_le fun i j => ?_
rcases h i j with ⟨k, hk⟩
exact le_iSup_of_le k hk
