English
A reversal symmetry for Ico: with suitable parameters, ∏_{j∈Ico k m} f(n−j) equals ∏_{j∈Ico (n+1−m) (n+1−k)} f(j).
Русский
Симметрия отражения для Ico.
LaTeX
$$$$ \\displaystyle \\prod_{j \\in \\mathrm{Ico}(k,m)} f(n-j) = \\prod_{j \\in \\mathrm{Ico}(n+1-m,\,n+1-k)} f(j). $$$$
Lean4
theorem prod_Ico_reflect (f : ℕ → M) (k : ℕ) {m n : ℕ} (h : m ≤ n + 1) :
(∏ j ∈ Ico k m, f (n - j)) = ∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j :=
by
have : ∀ i < m, i ≤ n := by
intro i hi
exact (add_le_add_iff_right 1).1 (le_trans (Nat.lt_iff_add_one_le.1 hi) h)
rcases lt_or_ge k m with hkm | hkm
· rw [← Nat.Ico_image_const_sub_eq_Ico (this _ hkm)]
refine (prod_image ?_).symm
simp only [mem_Ico, Set.InjOn, mem_coe]
rintro i ⟨_, im⟩ j ⟨_, jm⟩ Hij
rw [← tsub_tsub_cancel_of_le (this _ im), Hij, tsub_tsub_cancel_of_le (this _ jm)]
· have : n + 1 - k ≤ n + 1 - m := by
rw [tsub_le_tsub_iff_left h]
exact hkm
simp only [hkm, Ico_eq_empty_of_le, prod_empty, Ico_eq_empty_of_le this]
