prod_Ioo_cast — Mathlib

English

Let h : n = m and f : Fin m → M. The product over Ioo(cast h a)(cast h b) equals the product over Ioo a b with indices cast by h.

Русский

Пусть h: n=m и f: Fin m → M. Произведение по Ioo(cast h a)(cast h b) равно произведению по Ioo a b с индексацией через h.

LaTeX

$$$\displaystyle \prod_{i \in \mathrm{Ioo}(\mathrm{cast}(h,a),\mathrm{cast}(h,b))} f(i) = \prod_{i \in \mathrm{Ioo}(a,b)} f(i \mathrm{ cast } h).$$$

Lean4

@[to_additive]
theorem prod_Ioo_cast (h : n = m) (f : Fin m → M) (a b : Fin n) :
    ∏ i ∈ Ioo (a.cast h) (b.cast h), f i = ∏ i ∈ Ioo a b, f (i.cast h) := by simp [← map_finCongr_Ioo]

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