finprod_mem_mulSupport — Mathlib

English

The finprod over the support of f equals the unrestricted finprod: ∏ᶠ a ∈ mulSupport f, f(a) = ∏ᶠ a, f(a).

Русский

Финпроизводство по опоре функции равно общему финпроизводству: ∏ᶠ a ∈ mulSupport f, f(a) = ∏ᶠ a, f(a).

LaTeX

$$$$ \prod^{\mathrm{fin}}_{a \in \mathrm{mulSupport}(f)} f(a) = \prod^{\mathrm{fin}}_{a} f(a). $$$$

Lean4

@[to_additive]
theorem finprod_mem_mulSupport (f : α → M) : ∏ᶠ a ∈ mulSupport f, f a = ∏ᶠ a, f a := by
  rw [finprod_mem_def, mulIndicator_mulSupport]

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