mathlib3
35ecc7ba - feat(analysis/calculus): Rolle's and Cauchy's mean value theorems with weaker assumptions (deps : 3590) (#3681)

Commit
5 years ago
feat(analysis/calculus): Rolle's and Cauchy's mean value theorems with weaker assumptions (deps : 3590) (#3681) This introduces stronger versions of Rolle's theorem and Cauchy's mean value theorem, essentially by encapsulating an extension by continuity using the newly introduced `extend_from` of #3590 Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Author
Parents
Loading