finprod_eq_prod_plift_of_mulSupport_subset

English

If hf ⊆ s as Finsets, then the finprod f equals the product over s of f i.down.

Русский

Если hf ⊆ s как конечное множество, то финпроизводство равно произведению по i из s от f i.down.

LaTeX

$$$\\text{If } hf \\subseteq s,\\quad \\mathrm{finprod}(f) = \\prod_{i\\in s} f(i\\downarrow)$$$

Lean4

@[to_additive]
theorem finprod_eq_prod_plift_of_mulSupport_subset {f : α → M} {s : Finset (PLift α)}
    (hs : mulSupport (f ∘ PLift.down) ⊆ s) : ∏ᶠ i, f i = ∏ i ∈ s, f i.down :=
  finprod_eq_prod_plift_of_mulSupport_toFinset_subset (s.finite_toSet.subset hs) fun x hx =>
    by
    rw [Finite.mem_toFinset] at hx
    exact hs hx

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