finprod_eq_prod_of_mulSupport_subset

English

If f : α → M and s ⊆ α is such that mulSupport f ⊆ s, then ∏ᶠ i, f(i) = ∏ i ∈ s, f(i).

Русский

Если mulSupport f ⊆ s, то итоговое финпроизводство совпадает с конечным произведением по s.

LaTeX

$$$$ \prod^{\mathrm{fin}}_{i} f(i) = \prod_{i \in s} f(i). $$$$

Lean4

@[to_additive]
theorem finprod_eq_prod_of_mulSupport_subset (f : α → M) {s : Finset α} (h : mulSupport f ⊆ s) :
    ∏ᶠ i, f i = ∏ i ∈ s, f i :=
  by
  have A : mulSupport (f ∘ PLift.down) = Equiv.plift.symm '' mulSupport f :=
    by
    rw [mulSupport_comp_eq_preimage]
    exact (Equiv.plift.symm.image_eq_preimage _).symm
  have : mulSupport (f ∘ PLift.down) ⊆ s.map Equiv.plift.symm.toEmbedding :=
    by
    rw [A, Finset.coe_map]
    exact image_mono h
  rw [finprod_eq_prod_plift_of_mulSupport_subset this]
  simp only [Finset.prod_map, Equiv.coe_toEmbedding]
  congr

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