iSup_add_iSup_le — Mathlib

English

If for all i,j there exists k with f_i + g_j ≤ f_k + g_k, then iSup f + iSup g = ⨆ i, f_i + g_i.

Русский

Если для всех i,j существует k с f_i + g_j ≤ f_k + g_k, то (sup_i f_i) + (sup_j g_j) = sup_i (f_i + g_i).

LaTeX

$$$\\displaystyle \\text{If } \\forall i,j,\\; \\exists k:\\; f_i + g_j \\le f_k + g_k, \\\\; \\text{then } (\\sup_i f_i) + (\\sup_i g_i) = \\sup_i (f_i + g_i)$$$

Lean4

theorem iSup_add_iSup_le [Nonempty ι] [Nonempty κ] {g : κ → ℝ≥0∞} (h : ∀ i j, f i + g j ≤ a) : iSup f + iSup g ≤ a := by
  simp_rw [iSup_add, add_iSup]; exact iSup₂_le h

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