Commit 2022-04-21 15:19 8044794f

View on Github →

feat(topology/algebra/module/basic): continuous linear maps are automatically uniformly continuous (#13276) Generalize continuous_linear_map.uniform_continuous, continuous_linear_equiv.uniform_embedding and linear_equiv.uniform_embedding form normed_spaces to uniform_add_groups and move them to topology/algebra/module/basic.

Estimated changes

Modified src/analysis/normed_space/operator_norm.lean

deleted theorem continuous_linear_equiv.uniform_embedding

modified theorem continuous_linear_map.homothety_norm

modified theorem continuous_linear_map.op_norm_zero_iff

deleted theorem linear_equiv.uniform_embedding

modified theorem linear_isometry.norm_to_continuous_linear_map

modified theorem linear_isometry.norm_to_continuous_linear_map_comp

modified theorem linear_map.bound_of_shell

Modified src/topology/algebra/module/basic.lean

Modified src/topology/uniform_space/uniform_embedding.lean

added theorem equiv.uniform_embedding