Commit 2020-10-06 09:02 fc7e943e

View on Github →

feat(normed_space/basic): remove localized notation (#4246) Remove notation for tendsto in nhds. Also make is_bounded_linear_map.tendsto protected.

Estimated changes

Modified src/analysis/normed_space/basic.lean

modified theorem lim_norm

modified theorem lim_norm_zero

Modified src/analysis/normed_space/bounded_linear_maps.lean

deleted theorem is_bounded_linear_map.tendsto