innerSL — Mathlib

English

The inner product defines a continuous sesquilinear map when viewed as a map E × E → 𝕜.

Русский

Скалярное произведение задаёт непрерывную-селективную билинеарную форму при рассмотрении как отображение E × E → 𝕜.

LaTeX

$$$ inner_\\*, : E × E \\to 𝕜 \\text{ is sesquilinear and continuous }$$$

Lean4

/-- The inner product as a continuous sesquilinear map. Note that `toDualMap` (resp. `toDual`)
in `InnerProductSpace.Dual` is a version of this given as a linear isometry (resp. linear
isometric equivalence). -/
def innerSL : E →L⋆[𝕜] E →L[𝕜] 𝕜 :=
  LinearMap.mkContinuous₂ (innerₛₗ 𝕜) 1 fun x y => by simp only [norm_inner_le_norm, one_mul, innerₛₗ_apply]

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