Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-23 17:29 dd5074c4

View on Github →

feat(analysis/normed_space/basic): add has_nnnorm (#7986) We create here classes has_nndist and has_nnnorm that are variants of has_dist and has_norm taking values in ℝ≥0. Obvious instances are pseudo_metric_space and semi_normed_group. These are not used that much in mathlib, but for example has_nnnorm is quite convenient for LTE.

Estimated changes

modified theorem coe_nnnorm
modified theorem continuous.nnnorm
modified theorem continuous_at.nnnorm
modified theorem continuous_nnnorm
modified theorem continuous_on.nnnorm
modified theorem edist_eq_coe_nnnorm
modified theorem edist_eq_coe_nnnorm_sub
modified theorem mem_emetric_ball_0_iff
modified theorem nndist_eq_nnnorm
modified theorem nndist_nnnorm_nnnorm_le
deleted def nnnorm
modified theorem nnnorm_add_le
modified theorem nnnorm_eq_zero
modified theorem nnnorm_gsmul_le
modified theorem nnnorm_neg
modified theorem nnnorm_norm
modified theorem nnnorm_nsmul_le
modified theorem nnnorm_one
modified theorem nnnorm_smul
modified theorem nnnorm_zero
modified theorem nnreal.coe_nat_abs
modified theorem nnreal.nnnorm_eq
modified theorem normed_field.nnnorm_div
modified theorem normed_field.nnnorm_fpow
modified theorem normed_field.nnnorm_inv
modified theorem normed_field.nnnorm_mul
modified theorem normed_field.nnnorm_pow
modified theorem of_real_norm_eq_coe_nnnorm
modified theorem prod.nnnorm_def
modified theorem prod.nnsemi_norm_def
modified theorem real.ennnorm_eq_of_real
modified theorem real.nnnorm_coe_nat
modified theorem real.nnnorm_of_nonneg
modified theorem real.nnnorm_two
modified theorem real.norm_two
modified theorem summable_of_summable_nnnorm
modified theorem uniform_continuous_nnnorm
deleted def nndist