tprodL — Mathlib

English

Applying liftIsometry to tprodL yields the identity map on the tensor product space.

Русский

Применение liftIsometry к tprodL даёт тождественное отображение на тензорном произведении.

LaTeX

$$liftIsometry 𝕜 E F (tprodL 𝕜) = ContinuousLinearMap.id 𝕜 (⨂[𝕜] i, E i)$$

Lean4

/-- The canonical continuous multilinear map from `E = Πᵢ Eᵢ` to `⨂[𝕜] i, Eᵢ`.
-/
@[simps!]
noncomputable def tprodL : ContinuousMultilinearMap 𝕜 E (⨂[𝕜] i, E i) :=
  (liftIsometry 𝕜 E _).symm (ContinuousLinearMap.id 𝕜 _)

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