prod_Ici_succ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem prod_Ici_succ (f : Fin (n + 1) → M) (a : Fin n) : ∏ i ≥ a.succ, f i = ∏ i ≥ a, f i.succ := by
  simp [← map_succEmb_Ici]

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