Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-09 19:43 b39713fe

View on Github →

feat(analysis/calculus/darboux): IVT for derivatives (#2110)

feat(analysis/calculus/darboux): IVT for derivatives
whitespace Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr

Estimated changes

Created src/analysis/calculus/darboux.lean

added theorem convex_image_has_deriv_at

added theorem deriv_forall_lt_or_forall_gt_of_forall_ne

added theorem exists_has_deriv_within_at_eq_of_gt_of_lt

added theorem exists_has_deriv_within_at_eq_of_lt_of_gt

Modified src/analysis/calculus/local_extr.lean