map_finprod_of_injective — Mathlib

English

If g : M →* N is injective, then for every f : α → M we have g(∏ᶠ i, f(i)) = ∏ᶠ i, g(f(i)).

Русский

Если g : M →* N инъективен, то для любого f : α → M выполняется g(∏ᶠ i, f(i)) = ∏ᶠ i, g(f(i)).

LaTeX

$$$$ g\left(\prod^{\mathrm{fin}}_{i} f(i)\right) = \prod^{\mathrm{fin}}_{i} g\bigl(f(i)\bigr). $$$$

Lean4

@[to_additive]
theorem map_finprod_of_injective (g : M →* N) (hg : Injective g) (f : α → M) : g (∏ᶠ i, f i) = ∏ᶠ i, g (f i) :=
  g.map_finprod_of_preimage_one (fun _ => (hg.eq_iff' g.map_one).mp) f

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