mapLMultilinear — Mathlib

English

Scalar compatibility for mapL: mapL (update f i (c • u)) = c • mapL (update f i u) for a scalar c.

Русский

Совместимость по скаляру: 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

/-- The tensor of a family of linear maps from `Eᵢ` to `E'ᵢ`, as a continuous multilinear map of
the family.
-/
@[simps!]
noncomputable def mapLMultilinear :
    ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ E i →L[𝕜] E' i) ((⨂[𝕜] i, E i) →L[𝕜] ⨂[𝕜] i, E' i) :=
  MultilinearMap.mkContinuous
    { toFun := mapL
      map_update_smul' := fun _ _ _ _ ↦ PiTensorProduct.mapL_smul _ _ _ _
      map_update_add' := fun _ _ _ _ ↦ PiTensorProduct.mapL_add _ _ _ _ } 1
    (fun f ↦ by rw [one_mul]; exact mapL_opNorm f)

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