English
The finprod of a function f: α → M is defined by: if (mulSupport f).Finite, then it equals the finite product over a witness h.toFinset; otherwise it equals 1.
Русский
Финпроизводство функции f определяется как: если mulSupport f конечно, то это конечное произведение по некоторому witnesses; иначе равно 1.
LaTeX
$$$$ \prod^{\mathrm{fin}}_{i:\alpha} f(i) = \begin{cases} \prod_{i \in h.toFinset} f(i), & \text{if } (mulSupport f).Finite, \\ 1, & \text{otherwise}. \end{cases} $$$$
Lean4
@[to_additive]
theorem finprod_def (f : α → M) [Decidable (mulSupport f).Finite] :
∏ᶠ i : α, f i = if h : (mulSupport f).Finite then ∏ i ∈ h.toFinset, f i else 1 :=
by
split_ifs with h
· exact finprod_eq_prod_of_mulSupport_toFinset_subset _ h (Finset.Subset.refl _)
· rw [finprod, dif_neg]
rw [mulSupport_comp_eq_preimage]
exact mt (fun hf => hf.of_preimage Equiv.plift.surjective) h
