mapLMultilinear_opNorm — Mathlib

English

A variant of mapL_smul for a general scalar action: mapL (update f i (c • u)) = c • mapL (update f i u).

Русский

Вариант mapL_smul для общего действия скаляра: mapL (update f i (c • u)) = c • mapL (update f i u).

LaTeX

$$$ \\mathrm{mapL}(\\mathrm{update}\\, f\\, i\\, (c \\cdot u)) = c \\cdot \\mathrm{mapL}(\\mathrm{update}\\, f\\, i\\, u) $$$

Lean4

theorem mapLMultilinear_opNorm : ‖mapLMultilinear 𝕜 E E'‖ ≤ 1 :=
  MultilinearMap.mkContinuous_norm_le _ zero_le_one _

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