statement proposition
The exponential function is strictly increasing
Statement
The exponential function is strictly increasing on . That is, implies .
Remarks
The derivative is itself, and it is positive. Then positive derivative gives the claim.
Also as and as . So is a bijection from onto .
Mathlib states it as Real.exp_strictMono.
Explanations
L1 human
The exponential function always grows as grows. So it takes each positive value exactly once.
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 48 nodes in this order. The foundations come first, and the list ends with this node.
- Limit point of a set definition
- Local maximum definition
- Sequence definition
- Strictly monotone function definition
- Limit of a function definition
- Local minimum definition
- Real sequence definition
- Subsequence definition
- Continuity at a point definition
- Derivative definition
- Bounded sequence definition
- Geometric sequence definition
- Limit of a sequence definition
- Monotone sequence definition
- Series definition
- Continuous function definition
- Fermat's theorem on stationary points statement
- Sum of a finite geometric series statement
- Monotone convergence theorem for sequences statement
- Convergent sequence definition
- Every sequence has a monotone subsequence statement
- Squeeze theorem statement
- Cauchy product definition
- Partial sum definition
- Power series definition
- Bolzano–Weierstrass theorem statement
- The sequence r^n tends to zero for |r| < 1 example
- Radius of convergence definition
- Convergent series definition
- Boundedness theorem statement
- Absolute convergence definition
- A series of nonnegative terms converges iff its partial sums are bounded statement
- Sum of a series definition
- Extreme value theorem statement
- Comparison test statement
- Geometric series example
- Cauchy product of absolutely convergent series statement
- Rolle's theorem statement
- Ratio test statement
- Mean value theorem statement
- Ratio formula for the radius of convergence statement
- A function with positive derivative is strictly increasing statement
- The exponential series has infinite radius of convergence statement
- Exponential function definition
- Exponential of a sum statement
- The exponential function is positive statement
- The exponential function is its own derivative statement
- The exponential function is strictly increasing statement
What depends on this
18 nodes use this node, directly or through other nodes.
- Natural logarithm 0044CPHJBV
- Euler–Mascheroni constant 00C5P9JZBK
- The logarithm grows slower than any power 00DGYY10FV
- log x is at most x - 1 04CBRA4JRK
- Inverse hyperbolic functions 04D7CHT5V1
- Harmonic numbers grow like log n 05S2GSPMGA
- Derivative of the logarithm 07X1QA6BRW
- Logarithm of a quotient 0J7PHRBNNS
- Integral of 1/x 0K1N1Y4EGZ
- Logarithm of a product 0K2FNY6DYV
- Derivative of x^a 0KY08TWDMQ
- Logarithm is the inverse of the exponential 0RKW2X63YR
- Real exponentiation 0TV07AQT62
- Logarithm of a power 0V948DE5KA
- Improper integral of x^p on an unbounded interval 0VGKB2NC4T
- Integration by partial fractions 0WBTWFXJQG
- Mercator series 0YZXNE3HFR
- The logarithm is strictly concave 0ZS54B9GJF
Sources
What links here
Used by
- Natural logarithm 0044CPHJBV
- Logarithm is the inverse of the exponential 0RKW2X63YR