instNormedSpace — Mathlib

English

There is an isometric linear equivalence between ContinuousMultilinearMap 𝕜 E F and (⨂ i E i) →L F, induced by PiTensorProduct.lift.

Русский

Существует изометрическое линейное эквивалентное отображение между ContinuousMultilinearMap 𝕜 E F и (⨂ i E i) →L F, индуцируемое PiTensorProduct.lift.

LaTeX

$$liftIsometry 𝕜 E F : ContinuousMultilinearMap 𝕜 E F ≃ₗᵢ[𝕜] (⨂[𝕜] i, E i) →L[𝕜] F$$

Lean4

noncomputable instance : NormedSpace 𝕜 (⨂[𝕜] i, E i) where
  norm_smul_le a
    x := by
    change injectiveSeminorm.toFun (a • x) ≤ _
    rw [injectiveSeminorm.smul']
    rfl

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