biSup_add_biSup_le' — Mathlib

English

If f and g are monotone, then iSup f + iSup g equals iSup of (f i + g i).

Русский

Если f и g монотономы, то iSup f + iSup g равно iSup (f i + g i).

LaTeX

$$$ \text{Monotone } f \rightarrow \text{Monotone } g \rightarrow \mathrm{Eq}\big( \iSup f + \iSup g, \iSup_i (f_i + g_i)\big) $$$

Lean4

theorem biSup_add_biSup_le' {p : ι → Prop} {q : κ → Prop} (hp : ∃ i, p i) (hq : ∃ j, q j) {g : κ → ℕ∞}
    (h : ∀ i, p i → ∀ j, q j → f i + g j ≤ a) : (⨆ i, ⨆ _ : p i, f i) + ⨆ j, ⨆ _ : q j, g j ≤ a :=
  by
  simp_rw [biSup_add' hp, add_biSup' hq]
  exact iSup₂_le fun i hi => iSup₂_le (h i hi)

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