The topological dual of a normed space #
For base field
𝕜 = ℝ or
𝕜 = ℂ, this map is actually an isometric embedding; we provide a
normed_space.inclusion_in_double_dual_li of the map which is of type a bundled linear
E →ₗᵢ[𝕜] (dual 𝕜 (dual 𝕜 E)).
The inclusion of a normed space in its double (topological) dual, considered as a bounded linear map.
If one controls the norm of every
f x, then one controls the norm of
The inclusion of a normed space in its double dual is an isometry onto its image.