English
Let f: ι → α → ℝ≥0∞ and a finite nonempty index set s ⊆ α. If for every finite subset t ⊆ α and every i, j ∈ ι there exists k ∈ ι such that for all a ∈ t we have f(k,a) ≤ f(i,a) and f(k,a) ≤ f(j,a), then
Русский
Пусть f: ι → α → ℝ≥0∞ и s ⊆ α конечное непустое множество индексов. Если для каждого конечного подмножества t ⊆ α и любых i, j ∈ ι существует k ∈ ι такой, что для всех a ∈ t выполняется f(k,a) ≤ f(i,a) и f(k,a) ≤ f(j,a), то
LaTeX
$$$\left(\forall (t : \mathrm{Finset}\ \alpha) (i\ j : \iota), \exists k, \forall a \in t, f(k,a) \le f(i,a) \land f(k,a) \le f(j,a)\right) \Rightarrow
\inf_i \sum_{a\in s} f(i,a) = \sum_{a\in s} \inf_i f(i,a)$$$
Lean4
theorem iInf_sum {ι α : Type*} {f : ι → α → ℝ≥0∞} {s : Finset α} [Nonempty ι]
(h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a) :
⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a := by
induction s using Finset.cons_induction_on with
| empty => simp only [Finset.sum_empty, ciInf_const]
| cons a s ha ih =>
simp only [Finset.sum_cons, ← ih]
refine (iInf_add_iInf fun i j => ?_).symm
refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_
rw [Finset.forall_mem_cons] at hk
exact add_le_add hk.1.1 (Finset.sum_le_sum fun a ha => (hk.2 a ha).2)
