mapL_mul — Mathlib

English

The mapL construction preserves pointwise multiplication: mapL (f1 i * f2 i) = mapL f1 · mapL f2.

Русский

MapL сохраняет покомпонентное произведение: mapL (f1 i · f2 i) = mapL f1 · mapL f2.

LaTeX

$$$ \\mathrm{mapL}(\\lambda i, f_1 i \\cdot f_2 i) = (\\mathrm{mapL} f_1) \\cdot (\\mathrm{mapL} f_2) $$$

Lean4

theorem mapL_mul (f₁ f₂ : Π i, E i →L[𝕜] E i) : mapL (fun i ↦ f₁ i * f₂ i) = mapL f₁ * mapL f₂ :=
  mapL_comp f₁ f₂

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