English
Let s be a finite set and f: α → ι → ℝ≥0∞. 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: α → ι → ℝ≥0∞. Если для любых i,j ∈ ι существует k с ∀ a: f(a,i) ≤ f(a,k) и f(a,j) ≤ f(a,k), то
LaTeX
$$$\sum_{a\in s} \sup_i f(a,i) = \sup_{i} \sum_{a\in s} f(a,i)$$$
Lean4
theorem finsetSum_iSup {α ι : Type*} {s : Finset α} {f : α → ι → ℝ≥0∞}
(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]
