Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-28 15:08 39ffeab1

View on Github →

feat(analysis): add normed spaces

Estimated changes

added theorem abs_norm_sub_norm_le
added theorem coe_nnnorm
added theorem continuous_norm
added theorem dist_eq_norm
added theorem dist_norm_norm_le
added theorem dist_zero_right
added theorem lim_norm
added theorem lim_norm_zero
added theorem nndist_eq_nnnorm
added def nnnorm
added theorem nnnorm_eq_zero
added theorem nnnorm_neg
added theorem nnnorm_smul
added theorem nnnorm_triangle
added theorem nnnorm_zero
added theorem norm_eq_zero
added theorem norm_fst_le
added theorem norm_le_zero_iff
added theorem norm_mul
added theorem norm_neg
added theorem norm_nonneg
added theorem norm_pos_iff
added theorem norm_smul
added theorem norm_snd_le
added theorem norm_triangle
added theorem norm_zero
added theorem squeeze_zero
added theorem tendsto_smul