Mathlib v3 is deprecated. Go to Mathlib v4

Theorem normed_space.inclusion_in_double_dual_isometry

Modification history

2021-10-06 08:03
src/analysis/normed_space/dual.lean
refactor(analysis/{normed_space, inner_product_space}/dual): redefine using `linear_isometry` (#9569) …
Deleted normed_space.inclusion_in_double_dual_isometryView on Github →
2020-08-17 20:43
src/analysis/normed_space/dual.lean
feat(analysis/normed_space): generalize corollaries of Hahn-Banach (#3658)
Modified normed_space.inclusion_in_double_dual_isometryView on Github →
2020-06-14 12:37
src/analysis/normed_space/dual.lean
feat(normed_space/dual): (topological) dual of a normed space (#3021) …
Added normed_space.inclusion_in_double_dual_isometryView on Github →