Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-30 10:24 9a1ffe49

View on Github →

refactor(analysis/calculus/darboux): review API (#19125) Add more versions of the main theorem, slightly generalize existing versions.

Estimated changes

Modified src/analysis/calculus/darboux.lean

added theorem convex.image_deriv

added theorem convex.image_deriv_within

added theorem convex.image_has_deriv_within_at

deleted theorem convex_image_has_deriv_at

deleted theorem deriv_forall_lt_or_forall_gt_of_forall_ne

added theorem exists_has_deriv_within_at_eq_of_ge_of_le

added theorem exists_has_deriv_within_at_eq_of_le_of_ge

added theorem has_deriv_within_at_forall_lt_or_forall_gt_of_forall_ne

added theorem set.ord_connected.image_deriv

added theorem set.ord_connected.image_deriv_within

added theorem set.ord_connected.image_has_deriv_within_at