iSup_add_iSup_of_monotone — 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 iSup_add_iSup_of_monotone {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {f g : ι → ℕ∞} (hf : Monotone f)
    (hg : Monotone g) : iSup f + iSup g = ⨆ a, f a + g a :=
  iSup_add_iSup fun i j ↦ (exists_ge_ge i j).imp fun _k ⟨hi, hj⟩ ↦ by gcongr <;> apply_rules

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