iSup_add_iSup_le — Mathlib

English

If there exist i and j such that for all i,j, f i + g j ≤ a, then iSup f + iSup g ≤ a.

Русский

Если существуют i и j такие, что для всех i,j выполняется f(i) + g(j) ≤ a, тогда iSup f + iSup g ≤ a.

LaTeX

$$$ [Nonempty \i] [Nonempty \kappa] \{g : \kappa \to ENat\} (h : \forall i j, f i + g j ≤ a) : iSup f + iSup g ≤ a $$$

Lean4

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

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