Commit 2024-10-23 23:43 45deead3

View on Github →

feat: add First Derivative Test from calculus (#16802) Add proofs of the First Derivative Test, in max and min forms, using neighborhood filters. New branch due to merge conflict in the old branch.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/FirstDerivativeTest.lean

added theorem isLocalMax_of_deriv'

added theorem isLocalMax_of_deriv

added theorem isLocalMax_of_deriv_Ioo

added theorem isLocalMin_of_deriv'

added theorem isLocalMin_of_deriv

added theorem isLocalMin_of_deriv_Ioo

Modified Mathlib/Topology/ContinuousOn.lean

added theorem ContinuousOn.union_continuousAt

added theorem nhds_eq_nhdsWithin_sup_nhdsWithin

added theorem nhds_of_Ici_Iic

added theorem punctured_nhds_eq_nhdsWithin_sup_nhdsWithin

added theorem union_mem_nhds_of_mem_nhdsWithin

Modified Mathlib/Topology/Order/LocalExtr.lean

added theorem isLocalMax_of_mono_anti'

added theorem isLocalMin_of_anti_mono'

Created Mathlib/Topology/Order/OrderClosedExtr.lean

added theorem isLocalMax_of_mono_anti

added theorem isLocalMin_of_anti_mono