---
tag: 0KN2V7840E
kind: statement
role: proposition
name: The exponential function is strictly increasing
msc: [33B10]
uses: [0EX9GFJ0B3, 0P9BNBW2W3, 07J5X2T1ZX]
sources:
  - url: https://en.wikipedia.org/wiki/Exponential_function
    locator: Properties
---

## Statement

The exponential function is strictly increasing on $\mathbb{R}$.
That is, $x < y$ implies $\exp(x) < \exp(y)$.

## Remarks

The derivative is [[$\exp$ itself|0EX9GFJ0B3]], and it is [[positive|0P9BNBW2W3]]. Then [[positive derivative|07J5X2T1ZX]] gives the claim.
Also $\exp(x) \to \infty$ as $x \to \infty$ and $\exp(x) \to 0$ as $x \to -\infty$. So $\exp$ is a bijection from $\mathbb{R}$ onto $(0, \infty)$.
Mathlib states it as `Real.exp_strictMono`.

## Explanations

### L1 human

The exponential function always grows as $x$ grows.
So it takes each positive value exactly once.