tsum_eq_iSup_sum' — Mathlib

English

For a function f: α → β → ENNReal, the double sum over a bipartite indexing equals the iterated sums: ∑' p, f p.fst p.snd = ∑' a ∑' b, f a b.

Русский

Суммирование по функции f(a,b) разложимо: сумма по паре (a,b) равна двукратному суммированию.

LaTeX

$$$\\sum' p : \\Sigma a, b, f(p.fst,p.snd) = \\sum' a, \\sum' b, f(a,b).$$$

Lean4

protected theorem tsum_eq_iSup_sum' {ι : Type*} (s : ι → Finset α) (hs : ∀ t, ∃ i, t ⊆ s i) :
    ∑' a, f a = ⨆ i, ∑ a ∈ s i, f a := by
  rw [ENNReal.tsum_eq_iSup_sum]
  symm
  change ⨆ i : ι, (fun t : Finset α => ∑ a ∈ t, f a) (s i) = ⨆ s : Finset α, ∑ a ∈ s, f a
  exact (Finset.sum_mono_set f).iSup_comp_eq hs

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