A function with zero derivative is constant
Builds on Mean value theorem
Statement
Let be an open interval and let be differentiable with for all . Then is constant on .
Remarks
For in , the mean value theorem gives .
The domain must be an interval. On , a function equal to on one part and on the other has zero derivative.
So two antiderivatives of a function on an interval differ by a constant. Mathlib states the result as is_const_of_deriv_eq_zero.
Reading path
To understand this page from the ground up, read these 23 pages in order. The foundations come first.
Show the path as a graph
- no evidence level
- Limit point of a set definition
- Local maximum definition
- Sequence definition
- Limit of a function definition
- Local minimum definition
- Real sequence definition
- Subsequence definition
- Continuity at a point definition
- Derivative definition
- Bounded sequence definition
- Limit of a sequence definition
- Monotone sequence definition
- Continuous function definition
- Fermat's theorem on stationary points statement
- Convergent sequence definition
- Monotone convergence theorem for sequences statement
- Every sequence has a monotone subsequence statement
- Bolzano–Weierstrass theorem statement
- Boundedness theorem statement
- Extreme value theorem statement
- Rolle's theorem statement
- Mean value theorem statement
- A function with zero derivative is constant statement
Where this leads
9 pages build on this one.
Further reading
- Web https://en.wikipedia.org/wiki/Mean_value_theorem, Implications
About this page
| Tag | 003QDZ4T16 |
|---|---|
| URI | m2://003QDZ4T16 |
| Kind | statement, corollary |
| Writing | W0 stub |
| MSC | 26A24 |
| Status | This copy of the site has no build data. Run m2 status 003QDZ4T16. |
| Uses | Mean value theorem |
Markdown · JSON · Edit on GitHub
What this page needs for W1
- an inventory row: the row of the inventory that the node accounts for (0 of 1)
The writing levels say how complete the text of a page is. They do not measure its truth.