Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-03 06:31 879bad2e

View on Github →

feat(analysis/normed_space/enorm): define extended norm (#2897)

Estimated changes

Modified src/analysis/normed_space/basic.lean

modified theorem nnnorm_eq_zero

added theorem normed_field.nnnorm_inv

added theorem normed_field.nnnorm_one

added theorem real.nnnorm_coe_nat

added theorem real.nnnorm_two

added theorem real.norm_coe_nat

modified theorem real.norm_eq_abs

modified theorem real.norm_two

Created src/analysis/normed_space/enorm.lean

added theorem enorm.coe_fn_injective

added theorem enorm.coe_max

added def enorm.emetric_space

added theorem enorm.eq_zero_iff

added theorem enorm.ext

added theorem enorm.ext_iff

added theorem enorm.finite_dist_eq

added theorem enorm.finite_edist_eq

added theorem enorm.finite_norm_eq

added def enorm.finite_subspace

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