map_finprod — Mathlib

English

A more general version of map_finprod_mem requiring that s ∩ mulSupport f is finite; the image under a monoid hom g equals the finprod of g(f i).

Русский

Обобщенная версия map_finprod_mem': если s∩mulSupport f конечно, то отображение через г сохраняет финпроизведение.

LaTeX

$$$\\displaystyle g\\left(\\prod\\ᶠ j \\in s, f j\\right) = \\prod\\ᶠ i \\in s, g(f i)\\quad \\text{given } (s ∩ mulSupport f).Finite$$$

Lean4

@[to_additive]
theorem map_finprod {f : α → M} (g : M →* N) (hf : (mulSupport f).Finite) : g (∏ᶠ i, f i) = ∏ᶠ i, g (f i) :=
  g.map_finprod_plift f <| hf.preimage Equiv.plift.injective.injOn

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