continuousLinearMapOfBilin — Mathlib

English

A bounded sesquilinear form B on E corresponds to a continuous linear map B♯ : E → E, uniquely characterized by ⟪B♯v, w⟫ = Bv w for all v,w.

Русский

Пусть B — ограниченная бисемиляторная форма на E. Тогда существует непрерывное линейное отображение B♯: E → E, такое что для всех v,w выполняется ⟪B♯v, w⟫ = Bv w.

LaTeX

$$Definition: continuousLinearMapOfBilin(B) : E →L[𝕜] E$$

Lean4

/-- Maps a bounded sesquilinear form to its continuous linear map,
given by interpreting the form as a map `B : E →L⋆[𝕜] StrongDual 𝕜 E`
and dualizing the result using `toDual`.
-/
def continuousLinearMapOfBilin (B : E →L⋆[𝕜] E →L[𝕜] 𝕜) : E →L[𝕜] E :=
  (toDual 𝕜 E).symm.toContinuousLinearEquiv.toContinuousLinearMap.comp B

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