You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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;
- `exists_local_extr_Ioo`:
- rename to `exists_isLocalExtr_Ioo`;
- generalize as above;
- make `f` implicit;
- `exists_isExtrOn_Ioo_of_tendsto`, `exists_isLocalExtr_Ioo_of_tendsto`:
new lemmas extracted from the proof of `exists_hasDerivAt_eq_zero'`;
- `exists_hasDerivAt_eq_zero`, `exists_hasDerivAt_eq_zero'`:
make `f` and `f'` implicit;
- `exists_deriv_eq_zero`, `exists_deriv_eq_zero'`:
make `f` implicit.
I did it in leanprover-community/mathlib#19124 but decided not to
merge it before the port is done.
The text was updated successfully, but these errors were encountered: