Commit 2023-06-08 04:34 7c00d96b

View on Github →

feat: port Analysis.NormedSpace.ENorm (#3469)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/ENorm.lean

added theorem ENorm.coeFn_injective

added theorem ENorm.coe_inj

added theorem ENorm.coe_max

added def ENorm.emetricSpace

added theorem ENorm.eq_zero_iff

added theorem ENorm.ext

added theorem ENorm.ext_iff

added def ENorm.finiteSubspace

added theorem ENorm.finite_dist_eq

added theorem ENorm.finite_edist_eq

added theorem ENorm.finite_norm_eq

added theorem ENorm.map_add_le

added theorem ENorm.map_neg

added theorem ENorm.map_smul

added theorem ENorm.map_sub_le

added theorem ENorm.map_sub_rev

added theorem ENorm.map_zero

added theorem ENorm.max_map

added theorem ENorm.top_map

added structure ENorm