English
Let s be a finite set and f: s → (ι → ENat) a family; under a mild directedness assumption, the sum of iSup over s equals the iSup of sums: ∑_{a∈s} sup_i f(a,i) = sup_i ∑_{a∈s} f(a,i).
Русский
Пусть s — конечное множество и f: s → (ι → ENat) семейство; при мягком условии направляемости сумма iSup по s равна iSup сумм: ∑_{a∈s} ⨆_i f(a,i) = ⨆_i ∑_{a∈s} f(a,i).
LaTeX
$$$$ \\sum_{a \\in s} \\big( \\big( \\sup_i f(a,i) \\big) \\big) = \\sup_i \\sum_{a \in s} f(a,i) $$$$
Lean4
theorem sum_iSup {α ι : Type*} {s : Finset α} {f : α → ι → ℕ∞} (hf : ∀ i j, ∃ k, ∀ a, f a i ≤ f a k ∧ f a j ≤ f a k) :
∑ a ∈ s, ⨆ i, f a i = ⨆ i, ∑ a ∈ s, f a i := by
induction s using Finset.cons_induction with
| empty => simp
| cons a s ha ihs =>
simp_rw [Finset.sum_cons, ihs]
refine iSup_add_iSup fun i j ↦ (hf i j).imp fun k hk ↦ ?_
gcongr
exacts [(hk a).1, (hk _).2]
