statement corollary
A function with zero derivative is constant
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.
Explanations
L1 human
A function whose slope is zero everywhere on an interval never rises or falls. So its graph is a horizontal line.
What this node 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 node is. They do not measure its truth.
What this needs
To read this node, read these 23 nodes in this order. The foundations come first, and the list ends with this node.
- 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
What depends on this
9 nodes use this node, directly or through other nodes.
- cos pi = -1 01A8JGR4JM
- Pythagorean trigonometric identity 03H7WZ4T3K
- Derivative of arctangent 05P4B4Q22V
- Trigonometric substitution 0EAR3KNRTN
- Derivative of arcsine 0GA6G43EA9
- Sine is 2π-periodic 0P4NQD746K
- Power-reduction formula for cosine 0S049HG1W5
- Derivative of tangent 0SAMR34WXC
- Power series of arctangent 0T32ME0A6H
Sources
- Web https://en.wikipedia.org/wiki/Mean_value_theorem, Implications
What links here
Used by
- Pythagorean trigonometric identity 03H7WZ4T3K