prod_Ioi_succ — Mathlib

English

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

Русский

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

LaTeX

$$$$\\prod_{i \\in Ioi(a.succ)} f(i) = \\prod_{i \\in Ioi(a)} f(i.succ).$$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_Ioi_succ (f : Fin (n + 1) → M) (a : Fin n) : ∏ i > a.succ, f i = ∏ i > a, f i.succ := by
  simp [← map_succEmb_Ioi]

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