Theorems · Definition · functional analysis

NormedSpace.inclusionInDoubleDual

(𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    (E : Type u_2) →
      [inst_1 : SeminormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → E →L[𝕜] StrongDual 𝕜 (StrongDual 𝕜 E)

The inclusion of a normed space in its double (topological) strong dual, considered as a bounded linear map.

Defined in

Mathlib.Analysis.Normed.Module.DoubleDual

Cited by

7 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldSeminormedAddCommGroupNormedSpace