Commit 2020-12-18 09:12 c4f673cb

View on Github →

chore(analysis/normed_space/basic): continuous_at.norm etc (#5411) Add variants of the lemma that the norm is continuous. Also rewrite a few proofs, and rename three lemmas:

lim_norm -> tendsto_norm_sub_self
lim_norm_zero -> tendsto_norm_zero
lim_norm_zero' -> tendsto_norm_zero'

Estimated changes

Modified src/analysis/calculus/fderiv.lean

Modified src/analysis/normed_space/basic.lean

added theorem continuous.nnnorm

modified theorem continuous.norm

added theorem continuous_at.nnnorm

added theorem continuous_at.norm

added theorem continuous_on.nnnorm

added theorem continuous_on.norm

added theorem continuous_within_at.nnnorm

added theorem continuous_within_at.norm

modified theorem filter.tendsto.nnnorm

modified theorem filter.tendsto.norm

deleted theorem lim_norm

deleted theorem lim_norm_zero

added theorem tendsto_norm

added theorem tendsto_norm_nhds_within_zero

added theorem tendsto_norm_sub_self

added theorem tendsto_norm_zero

Modified src/analysis/normed_space/bounded_linear_maps.lean

Modified src/analysis/specific_limits.lean

deleted theorem lim_norm_zero'

added theorem tendsto_norm_zero'

Modified src/topology/basic.lean

added theorem continuous.tendsto'