Commit 2023-07-26 10:47 eec218b4
View on Github →refactor: split Analysis.Calculus.LocalExtr
(#5944)
Also make f
/f'
arguments implicit in all versions of Rolle's Theorem.
Fixes #4830
API changes
exists_Ioo_extr_on_Icc
:- generalize from functions
f : ℝ → ℝ
to functions from a conditionally complete linear order to a linear order. - make
f
implicit;
- generalize from functions
exists_local_extr_Ioo
:- rename to
exists_isLocalExtr_Ioo
; - generalize as above;
- make
f
implicit;
- rename to
exists_isExtrOn_Ioo_of_tendsto
,exists_isLocalExtr_Ioo_of_tendsto
: new lemmas extracted from the proof ofexists_hasDerivAt_eq_zero'
;exists_hasDerivAt_eq_zero
,exists_hasDerivAt_eq_zero'
: makef
andf'
implicit;exists_deriv_eq_zero
,exists_deriv_eq_zero'
: makef
implicit.