finprod_eq_prod_plift_of_mulSupport_toFinset_subset

English

If the finite support of f∘PLift.down is contained in a Finset s, then the finprod over α equals the finite product over s of f i.down.

Русский

Если поддержка f∘PLift.down ограничена конечным множеством s, то финпроизводство совпадает с произведением по i ∈ s от f i.down.

LaTeX

$$$(\\mathrm{finprod}\\ f) = \\prod_{i \\in s} f(i\\downarrow)$, provided $hf$ Finite and $hf \\subseteq s$$$

Lean4

@[to_additive]
theorem finprod_eq_prod_plift_of_mulSupport_toFinset_subset {f : α → M} (hf : (mulSupport (f ∘ PLift.down)).Finite)
    {s : Finset (PLift α)} (hs : hf.toFinset ⊆ s) : ∏ᶠ i, f i = ∏ i ∈ s, f i.down :=
  by
  rw [finprod, dif_pos hf]
  refine Finset.prod_subset hs fun x _ hxf => ?_
  rwa [hf.mem_toFinset, notMem_mulSupport] at hxf

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