Mathlib v3 is deprecated. Go to Mathlib v4

Theorem has_fderiv_at_of_dominated_of_fderiv_le

Modification history

2021-11-22 18:50
src/analysis/calculus/parametric_integral.lean
feat(analysis/calculus/parametric_integral): generalize, rename (#10397) …
Deleted has_fderiv_at_of_dominated_of_fderiv_leView on Github →
2021-05-14 12:02
src/analysis/calculus/parametric_integral.lean
feat(analysis/calculus/parametric_integral): derivative of parametric integrals (#7437) …
Added has_fderiv_at_of_dominated_of_fderiv_leView on Github →