iSup_add_iSup_of_monotone — Mathlib

English

If f and g are monotone on a directed index set, then iSup f + iSup g = sup_a (f(a) + g(a)).

Русский

Если f и g монотонны на направленном множестве индексов, то iSup f + iSup g = ⨆_a (f(a) + g(a)).

LaTeX

$$$\\text{Monotone}(f) \\;\\land\\; \\text{Monotone}(g) \\Rightarrow \\operatorname{iSup}(f) + \\operatorname{iSup}(g) = \\bigl(\\sup_a (f(a) + g(a))\\bigr)$$$

Lean4

theorem iSup_add_iSup_of_monotone {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {f g : ι → ℝ≥0∞} (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

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