prod_Iio_castSucc — Mathlib

English

Let f: Fin(n+1) → M and a ∈ Fin n. Then the product over all indices i with i smaller than a.castSucc equals the product over all indices i smaller than a of f(i.castSucc).

Русский

Пусть f: Fin(n+1) → M и a ∈ Fin n. Тогда произведение по всем i, удовлетворяющим i < a.castSucc, равно произведению по i < a, от f(i.castSucc).

LaTeX

$$$$\\prod_{i < a.castSucc} f(i) = \\prod_{i < a} f(i.castSucc).$$$$

Lean4

@[to_additive]
theorem prod_Iio_castSucc (f : Fin (n + 1) → M) (a : Fin n) : ∏ i < a.castSucc, f i = ∏ i < a, f i.castSucc := by
  simp [← map_castSuccEmb_Iio]

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