Commit 2023-05-24 09:36 81616565

View on Github →

feat: port Analysis.NormedSpace.HahnBanach.Extension (#4268)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean

added theorem Real.exists_extension_norm_eq

added theorem coord_norm'

added theorem exists_dual_vector''

added theorem exists_dual_vector'

added theorem exists_dual_vector

added theorem exists_extension_norm_eq