prod_Icc_succ — Mathlib

English

Let f: Fin(n+1) → M and a,b ∈ Fin n. Then the product over i in Icc(a.succ, b.succ) equals the product over i in Icc(a, b) of f(i.succ).

Русский

Пусть f: Fin(n+1) → M и a,b ∈ Fin n. Тогда произведение по i в Icc(a.succ, b.succ) равно произведению по i в Icc(a, b) от f(i.succ).

LaTeX

$$$$\\prod_{i \\in Icc(a.succ, b.succ)} f(i) = \\prod_{i \\in Icc(a, b)} f(i.succ).$$$$

Lean4

@[to_additive]
theorem prod_Icc_succ (f : Fin (n + 1) → M) (a b : Fin n) : ∏ i ∈ Icc a.succ b.succ, f i = ∏ i ∈ Icc a b, f i.succ := by
  simp [← map_succEmb_Icc]

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