finprod_mem_eq_one_of_infinite — Mathlib

English

If the intersection of s with the multiplicative support of f is infinite, then the finprod over s of f equals 1.

Русский

Если пересечение s с мультипликативной опорой f бесконечно, то \$ \\prodᶠ i∈s f(i) = 1 \$.

LaTeX

$$$\\displaystyle \\Big( (s \\cap \\mathrm{mulSupport}(f)) \\text{ is infinite} \\Big) \\;\\Rightarrow\\; \\prod\\ᶠ i \\in s, f(i) = 1$$$

Lean4

@[to_additive]
theorem finprod_mem_eq_one_of_infinite {f : α → M} {s : Set α} (hs : (s ∩ mulSupport f).Infinite) : ∏ᶠ i ∈ s, f i = 1 :=
  by
  rw [finprod_mem_def]
  apply finprod_of_infinite_mulSupport
  rwa [← mulSupport_mulIndicator] at hs

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