Commit 2023-07-16 11:34 10c93ae2

View on Github →

chore: forward-port leanprover-community/mathlib#19103 (#5855)

Estimated changes

Modified Mathlib/Analysis/Calculus/FDeriv/Basic.lean

Modified Mathlib/Analysis/Normed/Group/Basic.lean

added theorem AntilipschitzWith.le_mul_nnnorm'

added theorem AntilipschitzWith.le_mul_norm'

added theorem LipschitzWith.nnorm_le_mul'

added theorem LipschitzWith.norm_le_mul'

deleted theorem MonoidHomClass.bound_of_antilipschitz

added theorem OneHomClass.bound_of_antilipschitz

added theorem dist_le_norm_add_norm'

deleted theorem dist_le_norm_mul_norm

Modified Mathlib/Analysis/NormedSpace/ContinuousLinearMap.lean