sum_iSup_of_monotone — Mathlib

English

If each a ∈ α defines a monotone map f(a): ι → ENat, then ∑_{a∈s} iSup_i f(a,i) = iSup_i ∑_{a∈s} f(a,i).

Русский

Если для каждого a ∈ α отображение f(a,i) по i монотонно, то сумма по a и i распр. с iSup: ∑_{a∈s} iSup_i f(a,i) = iSup_i ∑_{a∈s} f(a,i).

LaTeX

$$$$ \\sum_{a \\in s} \\big( \\big( i\\!\\!\\!\\! \\uparrow i \\big) f(a,i) \\big) = \\uparrow i \\; \\sum_{a \\in s} f(a,i) $$$$

Lean4

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

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