English
For natural numbers a ≤ b, the relationship ∏_{k∈Ico(a,b+1)} f(k) = (∏_{k∈Ico(a,b)} f(k))·f(b) holds.
Русский
Для натуральных a ≤ b верно: ∏_{k∈Ico(a,b+1)} f(k) = (∏_{k∈Ico(a,b)} f(k))·f(b).
LaTeX
$$$$ \\displaystyle \\prod_{k \in \\mathrm{Ico}(a,b+1)} f(k) = \\left(\\prod_{k \in \\mathrm{Ico}(a,b)} f(k)\\right) \\cdot f(b). $$$$
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 b, f i j) = ∑ j ∈ Finset.Ico a b, ∑ i ∈ Finset.Ico a (j + 1), 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
