English
Let M be a commutative monoid. For h : n ≤ m, a,b : Fin n, and f : Fin m → M, the product over i ∈ Ioo (a.castLE h) (b.castLE h) equals the product over i ∈ Ioo a b of f(i.castLE h).
Русский
Пусть M — коммутативный моноид. При h : n ≤ m, a,b : Fin n и f : Fin m → M произведение по i∈Ioo(a.castLE h)(b.castLE h) равно произведению по i∈Ioo a b от f(i.castLE h).
LaTeX
$$$$ \\displaystyle \\prod_{i \\in \\mathrm{Ioo}(a^{\\mathrm{castLE} h}, b^{\\mathrm{castLE} h})} f(i) = \\prod_{i \\in \\mathrm{Ioo} a b} f(i^{\\mathrm{castLE} h}) $$$$
Lean4
@[to_additive]
theorem prod_Ioo_castLE (h : n ≤ m) (f : Fin m → M) (a b : Fin n) :
∏ i ∈ Ioo (a.castLE h) (b.castLE h), f i = ∏ i ∈ Ioo a b, f (i.castLE h) := by simp [← map_castLEEmb_Ioo]
