map_finprod — Mathlib

English

Let F be a structure with EquivLike M N and MulEquivClass. Then for any g : F and f : α → M, we have g(∏ᶠ i, f(i)) = ∏ᶠ i, g(f(i)).

Русский

Пусть F обладает структурой EquivLike M N и MulEquivClass. Тогда для любого g : F и 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 {F : Type*} [EquivLike F M N] [MulEquivClass F M N] (g : F) (f : α → M) :
    g (∏ᶠ i, f i) = ∏ᶠ i, g (f i) :=
  MulEquiv.map_finprod (MulEquivClass.toMulEquiv g) f

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