finprod_mem_inter_mulSupport_eq — Mathlib

English

If s ∩ mulSupport f = t ∩ mulSupport f, then the finprod over s of f equals the finprod over t of f.

Русский

Если s ∩ mulSupport f = t ∩ mulSupport f, то \$ \\prodᶠ i∈s f(i) = \\prodᶠ i∈t f(i) \$.

LaTeX

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

Lean4

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

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