---
tag: 0D6FCW80A0
kind: statement
role: theorem
name: A continuous injective function on an interval is strictly monotone
msc: [26A48]
uses: [00KAFBR32E, 0TR9SR9FTB]
sources:
  - url: https://en.wikipedia.org/wiki/Monotonic_function
    locator: Inverse of function
---

## Statement

Let $I$ be an interval and let $f \colon I \to \mathbb{R}$ be continuous and injective.
Then $f$ is [[strictly monotone|0TR9SR9FTB]].

## Remarks

Suppose $x < y < z$ in $I$ with $f(y)$ not between $f(x)$ and $f(z)$. Then the [[intermediate value theorem|00KAFBR32E]] gives a value of $f$ taken twice, which contradicts injectivity.
Continuity is needed. The function on $[0, 2]$ with $f(x) = x$ for $x < 1$ and $f(x) = 3 - x$ for $x \ge 1$ is injective but not monotone.
Mathlib states a form for closed intervals as `ContinuousOn.strictMonoOn_of_injOn_Icc`.

## Explanations

### L1 human

A continuous function on an interval that goes up and then down would take some value twice.
So if it never repeats a value, it must always go up or always go down.
