prod_uIcc_succ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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