Theorems · Definition · functional analysis

InnerProductSpace.toDualMap

(𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : RCLike 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → E →ₗᵢ⋆[𝕜] StrongDual 𝕜 E

An element x of an inner product space E induces an element of the strong dual space StrongDual 𝕜 E, the map fun y => ⟪x, y⟫; moreover this operation is a conjugate-linear isometric embedding of E into StrongDual 𝕜 E. If E is complete, this operation is surjective, hence a conjugate-linear isometric equivalence; see toDual.

Defined in

Mathlib.Analysis.InnerProductSpace.Dual

Cited by

26 results in Mathlib

Foundations

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

Assumes

RCLikeSeminormedAddCommGroupInnerProductSpace