finprod_mem_eq_prod_filter — Mathlib

English

For f : α → M and a set s, with DecidablePred (i ∈ s), and hf : (mulSupport f).Finite, we have ∏ᶠ i ∈ s, f i = ∏ i ∈ hf.toFinset with i ∈ s, f i.

Русский

Для f: α → M и множества s с decidablePred, если mulSupport f конечна, то ∏ᶠ i ∈ s, f i = ∏ i ∈ hf.toFinset with i ∈ s, f i.

LaTeX

$$$$ \prod^{\mathrm{fin}}_{i \in s} f(i) = \left( \prod_{i \in hf.toFinset} f(i) \right)_{\text{with } i \in s}. $$$$

Lean4

@[to_additive]
theorem finprod_mem_eq_prod_filter (f : α → M) (s : Set α) [DecidablePred (· ∈ s)] (hf : (mulSupport f).Finite) :
    ∏ᶠ i ∈ s, f i = ∏ i ∈ hf.toFinset with i ∈ s, f i :=
  finprod_mem_eq_prod_of_inter_mulSupport_eq _ <| by
    ext x
    simp [and_comm]

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