Commit 2020-06-14 12:37 a6534db8
View on Github →feat(normed_space/dual): (topological) dual of a normed space (#3021)
Define the topological dual of a normed space, and prove that over the reals, the inclusion into the double dual is an isometry.
Supporting material: a corollary of Hahn-Banach; material about spans of singletons added to linear_algebra.basic
and normed_space.operator_norm
; material about homotheties added to normed_space.operator_norm
.