Commit 2023-07-12 18:27 41bef4ae

View on Github →

feat(analysis/normed/group/basic): norm lemmas for lipschitz and antilipschitz (#19103) This also corrects some nonsense names produced by to_additive.

Estimated changes

Modified src/analysis/calculus/fderiv/basic.lean

Modified src/analysis/normed/group/basic.lean

added theorem antilipschitz_with.le_mul_nnnorm'

added theorem antilipschitz_with.le_mul_norm'

modified theorem antilipschitz_with.le_mul_norm_div

added theorem dist_le_norm_add_norm'

deleted theorem dist_le_norm_mul_norm

added theorem lipschitz_with.nnorm_le_mul'

added theorem lipschitz_with.norm_le_mul'

deleted theorem monoid_hom_class.bound_of_antilipschitz

added theorem one_hom_class.bound_of_antilipschitz

Modified src/analysis/normed_space/continuous_linear_map.lean