prod_range_reflect — Mathlib

English

Reflecting the index in a range product yields the same total; a short lemma used in various proofs.

Русский

Отражение индекса в диапазонном произведении даёт тот же результат.

LaTeX

$$$$ \\displaystyle \\text{range reflect identity for products}. $$$$

Lean4

theorem prod_range_reflect (f : ℕ → M) (n : ℕ) : (∏ j ∈ range n, f (n - 1 - j)) = ∏ j ∈ range n, f j :=
  by
  cases n
  · simp
  · simp only [← Nat.Ico_zero_eq_range, Nat.succ_sub_succ_eq_sub, tsub_zero]
    rw [prod_Ico_reflect _ _ le_rfl]
    simp

Похожие утверждения