Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-17 20:43 f818acbe

View on Github →

feat(analysis/normed_space): generalize corollaries of Hahn-Banach (#3658)

Estimated changes

Modified src/analysis/normed_space/dual.lean

modified theorem normed_space.inclusion_in_double_dual_isometry

modified theorem normed_space.norm_le_dual_bound

Modified src/analysis/normed_space/hahn_banach.lean

modified theorem coord_norm'

deleted theorem coord_self'

modified theorem exists_dual_vector'

modified theorem exists_dual_vector

added theorem norm'_def

added theorem norm_norm'

Modified src/analysis/normed_space/operator_norm.lean

added theorem continuous_linear_equiv.coord_self