English
A symmetric identity for double sums over Ico shows an equivalent rearrangement. In particular, ∑_{i∈Ico a b} ∑_{j∈Ico (i+1) b} f(i,j) equals ∑_{j∈Ico a b} ∑_{i∈Ico a j} f(i,j).
Русский
Симметричное тождество для двойной суммы над Ico.
LaTeX
$$$$ \\displaystyle \\sum_{i \\in \\mathrm{Ico}(a,b)} \\sum_{j \\in \\mathrm{Ico}(i+1,b)} f(i,j) = \\sum_{j \\in \\mathrm{Ico}(a,b)} \\sum_{i \\in \\mathrm{Ico}(a,j)} f(i,j). $$$$
Lean4
@[to_additive]
theorem prod_Ico_eq_prod_range (f : ℕ → M) (m n : ℕ) : ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k) :=
by
by_cases h : m ≤ n
· rw [← Nat.Ico_zero_eq_range, prod_Ico_add, zero_add, tsub_add_cancel_of_le h]
· replace h : n ≤ m := le_of_not_ge h
rw [Ico_eq_empty_of_le h, tsub_eq_zero_iff_le.mpr h, range_zero, prod_empty, prod_empty]
