Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-26 19:07 d3c68fc6

View on Github →

feat(analysis/normed_space): tendsto_zero_iff_norm_tendsto_zero

Estimated changes

modified theorem continuous_norm
modified theorem lim_norm
modified theorem lim_norm_zero