finprod_eq_prod_of_fintype — Mathlib

English

Same as above: for any f, if hf finite, then finprod f equals the finite product over hf.toFinset.

Русский

То же самое: если hf конечен, то финпроизводство f равно произведению по hf.toFinset.

LaTeX

$$$$ \prod^{\mathrm{fin}}_{i} f(i) = \prod_{i \in hf.toFinset} f(i). $$$$

Lean4

@[to_additive]
theorem finprod_eq_prod_of_fintype [Fintype α] (f : α → M) : ∏ᶠ i : α, f i = ∏ i, f i :=
  finprod_eq_prod_of_mulSupport_toFinset_subset _ (Set.toFinite _) <| Finset.subset_univ _

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