Mathlib v3 is deprecated. Go to Mathlib v4

Theorem has_fderiv_at.le_of_lip

Modification history

2020-09-18 08:44
src/analysis/calculus/fderiv.lean
feat(analysis/calculus): converse mean value inequality (#4173) …
Added has_fderiv_at.le_of_lipView on Github →