statement theorem
Darboux's theorem
Statement
Let and let be differentiable on , with one-sided derivatives at the endpoints. Let be a real number strictly between and . Then there is with .
Remarks
Assume . The function has . So its minimum on , given by the extreme value theorem, is at an interior point . Fermat's theorem gives .
So a derivative has the intermediate value property, even when it is not continuous.
In particular, a derivative has no jump discontinuities. Mathlib states it as exists_hasDerivWithinAt_eq_of_gt_of_lt.
Explanations
L1 human
The derivative of a function cannot skip values, just as a continuous function cannot. For example, no function has derivative on the left of a point and on the right.
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
- One-sided limit definition
- Bounded sequence definition
- Limit of a sequence definition
- Monotone sequence definition
- Continuous function definition
- Fermat's theorem on stationary points statement
- One-sided derivative definition
- Convergent sequence definition
- Every sequence has a monotone subsequence statement
- Monotone convergence theorem for sequences statement
- Bolzano–Weierstrass theorem statement
- Boundedness theorem statement
- Extreme value theorem statement
- Darboux's theorem statement
What depends on this
1 node uses this node, directly or through other nodes.
Sources
- Web https://en.wikipedia.org/wiki/Darboux%27s_theorem_(analysis), Statement of the theorem