English
If for all i there exists k with f i + g i ≤ f k + g k, then iSup f + iSup g = iSup (f i + g i).
Русский
Если для каждого i существует k, такой что f_i + g_i ≤ f_k + g_k, тогда iSup f + iSup g = iSup (f_i + g_i).
LaTeX
$$$ (\forall i, \exists k, f_i + g_i ≤ f_k + g_k) \Rightarrow ( \iSup f + \iSup g = \iSup_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
