mapL_id — Mathlib

English

For a given continuous multilinear map h, the liftIsometry composed with mapL is equal to the liftIsometry after composing h with f: liftIsometry 𝕜 E' F h ∘L mapL f = liftIsometry 𝕜 E F (h ∘ContinuousLinearMap f).

Русский

Для данного непрерывного многолинейного отображения h верно: liftIsometry ∘ mapL f = liftIsometry после применения h к f.

LaTeX

$$$ \\mathrm{liftIsometry}_{𝕜} \\; E'\\; F\\; h \\circL \\mathrm{mapL} f = \\mathrm{liftIsometry}_{𝕜} \\; E\\; F\\; (h \\cdot f) $$$

Lean4

@[simp]
theorem mapL_id : mapL (fun i ↦ ContinuousLinearMap.id 𝕜 (E i)) = ContinuousLinearMap.id _ _ :=
  by
  apply ContinuousLinearMap.coe_injective
  ext
  simp only [mapL_coe, ContinuousLinearMap.coe_id, map_id, LinearMap.compMultilinearMap_apply, LinearMap.id_coe, id_eq]

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