mapL_add — Mathlib

English

The operator norm of mapL is bounded by the product of the operator norms of the coordinate maps: ||mapL f|| ≤ ∏_i ||f_i||.

Русский

Операторная норма mapL ограничена произведением норм операторов координат: ||mapL f|| ≤ ∏_i ||f_i||.

LaTeX

$$$ \\|\\mathrm{mapL} f\\| \\leq \\prod_i \\|f_i\\| $$$

Lean4

protected theorem mapL_add [DecidableEq ι] (i : ι) (u v : E i →L[𝕜] E' i) :
    mapL (update f i (u + v)) = mapL (update f i u) + mapL (update f i v) :=
  by
  ext x
  simp only [mapL_apply, mapL_add_smul_aux, ContinuousLinearMap.coe_add, PiTensorProduct.map_update_add,
    LinearMap.add_apply, ContinuousLinearMap.add_apply]

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