finsetSum_iSup_of_monotone — Mathlib

English

Let s be a finite set and f: α → ι → ENNReal. If for all i,j there exists k with ∀ a, f(a,i) ≤ f(a,k) ∧ f(a,j) ≤ f(a,k), then

Русский

Пусть s—конечное множество и f: α → ι → ENNReal. Если для любых i,j существует k с ∀ a: f(a,i) ≤ f(a,k) и f(a,j) ≤ f(a,k), то

LaTeX

$$$\sum_{a\in s} \iSup_i f(a,i) = \iSup_i \sum_{a\in s} f(a,i)$$$

Lean4

theorem finsetSum_iSup_of_monotone {α ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {s : Finset α} {f : α → ι → ℝ≥0∞}
    (hf : ∀ a, Monotone (f a)) : (∑ a ∈ s, iSup (f a)) = ⨆ n, ∑ a ∈ s, f a n :=
  finsetSum_iSup fun i j ↦ (exists_ge_ge i j).imp fun _k ⟨hi, hj⟩ a ↦ ⟨hf a hi, hf a hj⟩

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