Mathlib v3 is deprecated. Go to Mathlib v4

Theorem has_strict_fderiv_at.exists_lipschitz_on_with_of_nnnorm_lt

Modification history

2021-07-23 09:02
src/analysis/calculus/fderiv.lean
feat(analysis/calculus): strictly differentiable (or C^1) map is locally Lipschitz (#8362)
Added has_strict_fderiv_at.exists_lipschitz_on_with_of_nnnorm_ltView on Github →