Theorems · Definition · functional analysis

innerSL

(𝕜 : Type u_1) →
  {E : Type u_2} →
    [inst : RCLike 𝕜] → [inst_1 : SeminormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → E →L⋆[𝕜] E →L[𝕜] 𝕜

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).

Defined in

Mathlib.Analysis.InnerProductSpace.LinearMap

Cited by

93 results in Mathlib

Foundations

Depth 176 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeSeminormedAddCommGroupInnerProductSpace