Commit 2024-12-20 16:06 e5c7795a

View on Github →

feat: Define ENorm notation class (#20121)

This PR only defines the notation class and two instances, but doesn't use it yet.
There is an existing unused definition of ENorm. Since I might use it in the future, I kept it around, but renamed it (and the file) ENormedSpace. I did not modify anything, and didn't add deprecations since it is unused and the main definition now has a different meaning.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Normed/Group/Basic.lean

added theorem enorm_eq_nnnorm

added theorem enorm_eq_self

Renamed Mathlib/Analysis/NormedSpace/ENorm.lean to Mathlib/Analysis/NormedSpace/ENormedSpace.lean

deleted theorem ENorm.coeFn_injective

deleted theorem ENorm.coe_inj

deleted theorem ENorm.coe_max

deleted theorem ENorm.eq_zero_iff

deleted theorem ENorm.ext

deleted def ENorm.finiteSubspace

deleted theorem ENorm.finite_dist_eq

deleted theorem ENorm.finite_edist_eq

deleted theorem ENorm.finite_norm_eq

deleted theorem ENorm.map_add_le

deleted theorem ENorm.map_neg

deleted theorem ENorm.map_smul

deleted theorem ENorm.map_sub_le

deleted theorem ENorm.map_sub_rev

deleted theorem ENorm.map_zero

deleted theorem ENorm.max_map

deleted theorem ENorm.top_map

deleted structure ENorm

added theorem ENormedSpace.coeFn_injective

added theorem ENormedSpace.coe_inj

added theorem ENormedSpace.coe_max

added theorem ENormedSpace.eq_zero_iff

added theorem ENormedSpace.ext

added def ENormedSpace.finiteSubspace

added theorem ENormedSpace.finite_dist_eq

added theorem ENormedSpace.finite_edist_eq

added theorem ENormedSpace.finite_norm_eq

added theorem ENormedSpace.map_add_le

added theorem ENormedSpace.map_neg

added theorem ENormedSpace.map_smul

added theorem ENormedSpace.map_sub_le

added theorem ENormedSpace.map_sub_rev

added theorem ENormedSpace.map_zero

added theorem ENormedSpace.max_map

added theorem ENormedSpace.top_map

added structure ENormedSpace