finprod_mem_inter_mulSupport — Mathlib

English

The finprod over s ∩ mulSupport f equals the finprod over s of f.

Русский

Произведение по s∩mulSupport f равно произведению по s.

LaTeX

$$$\\displaystyle \\prod\\ᶠ i \\in s \\cap mulSupport(f),\\ f(i) = \\prod\\ᶠ i \\in s,\\ f(i)$$$

Lean4

@[to_additive]
theorem finprod_mem_inter_mulSupport (f : α → M) (s : Set α) : ∏ᶠ i ∈ s ∩ mulSupport f, f i = ∏ᶠ i ∈ s, f i := by
  rw [finprod_mem_def, finprod_mem_def, mulIndicator_inter_mulSupport]

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