Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-08 02:16 5bf92e1d

View on Github →

chore(analysis/calculus/local_extr): review (#6085)

  • golf 2 proofs;
  • don't use explicit section variables;
  • add 2 docstrings.

Estimated changes

modified theorem exists_Ioo_extr_on_Icc
modified theorem exists_deriv_eq_zero'
modified theorem exists_deriv_eq_zero
modified theorem exists_has_deriv_at_eq_zero
modified theorem exists_local_extr_Ioo