statement theorem
One-sided limits of a monotone function exist
Statement
Let and let be increasing. Then both one-sided limits of at exist, and
Remarks
The proof is the same as for the monotone convergence theorem. The supremum exists because is an upper bound.
A similar statement holds for decreasing functions, with the inequalities reversed.
So is continuous at exactly when the two one-sided limits are equal. Otherwise is a jump discontinuity.
Mathlib states the left limit as Monotone.tendsto_nhdsLT.
Explanations
L1 human
An increasing function can only move up as approaches from the left. Its values are bounded by , so they settle at a limit.
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 10 nodes in this order. The foundations come first, and the list ends with this node.
- no evidence level
- Limit point of a set definition
- Sequence definition
- Limit of a function definition
- Real sequence definition
- One-sided limit definition
- Bounded sequence definition
- Limit of a sequence definition
- Monotone sequence definition
- Monotone convergence theorem for sequences statement
- One-sided limits of a monotone function exist statement
What depends on this
28 nodes use this node, directly or through other nodes.
- Euler–Mascheroni constant 00C5P9JZBK
- Inverse trigonometric functions 02HTDK1FBD
- log x is at most x - 1 04CBRA4JRK
- Derivative of arctangent 05P4B4Q22V
- Harmonic numbers grow like log n 05S2GSPMGA
- Arctangent 065XW2V6C3
- Continuity of the inverse of a strictly monotone continuous function 07BY47HG5S
- Derivative of the logarithm 07X1QA6BRW
- Arcsine 0B89D93YA1
- Gaussian integral 0DFT1GP1JP
- The gamma function extends the factorial 0FDCW77H44
- Comparison test for improper integrals 0FR1BDKK10
- Derivative of arcsine 0GA6G43EA9
- Logarithm of a quotient 0J7PHRBNNS
- Integral of 1/x 0K1N1Y4EGZ
- Logarithm of a product 0K2FNY6DYV
- Derivative of x^a 0KY08TWDMQ
- Derivative of an inverse function 0M0RZ3HSB0
- Arccosine 0RDP2HEFEW
- Logarithm is the inverse of the exponential 0RKW2X63YR
- Power series of arctangent 0T32ME0A6H
- Gamma function 0V3FZMVB4K
- Logarithm of a power 0V948DE5KA
- Improper integral of x^p on an unbounded interval 0VGKB2NC4T
- Integration by partial fractions 0WBTWFXJQG
- A monotone function has countably many discontinuities 0WYTM4C9QG
- Mercator series 0YZXNE3HFR
- The logarithm is strictly concave 0ZS54B9GJF
Sources
- Web https://en.wikipedia.org/wiki/Monotonic_function, Some basic applications and results