prod_Ioc_succ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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