Mathlib v3 is deprecated. Go to Mathlib v4

Theorem has_fderiv_at.le_of_lip'

Modification history

2021-11-22 18:50
src/analysis/calculus/fderiv.lean
feat(analysis/calculus/parametric_integral): generalize, rename (#10397) …
Added has_fderiv_at.le_of_lip'View on Github →