English
The two natural orderings of summing over pairs in a triangular region defined by a ≤ i ≤ j < b yield the same total: ∑_{i∈Ico a b} ∑_{j∈Ico i b} f(i,j) = ∑_{j∈Ico a b} ∑_{i∈Ico a (j+1)} f(i,j).
Русский
Суммирование по парам в треугольнике даёт одно и то же значение независимо от порядка, т. е. ∑∑ одинаково.
LaTeX
$$$$ \\displaystyle \\sum_{i \in \\mathrm{Ico}(a,b)} \\sum_{j \in \\mathrm{Ico}(i,b)} f(i,j) = \\sum_{j \in \\mathrm{Ico}(a,b)} \\sum_{i \in \\mathrm{Ico}(a,j+1)} f(i,j). $$$$
Lean4
/-- The two ways of summing over `(i, j)` in the range `a ≤ i < j < b` are equal. -/
theorem sum_Ico_Ico_comm' {M : Type*} [AddCommMonoid M] (a b : ℕ) (f : ℕ → ℕ → M) :
(∑ i ∈ Finset.Ico a b, ∑ j ∈ Finset.Ico (i + 1) b, f i j) = ∑ j ∈ Finset.Ico a b, ∑ i ∈ Finset.Ico a j, f i j :=
by
rw [Finset.sum_sigma', Finset.sum_sigma']
refine sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) ?_ ?_ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) <;>
simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma] <;>
omega
