---
tag: 0P64VE79X3
kind: statement
role: corollary
name: A function with bounded derivative is Lipschitz
msc: [26A16]
uses: [0BARQY52N5, 0QNVQ4VD9T]
sources:
  - url: https://en.wikipedia.org/wiki/Lipschitz_continuity
    locator: Examples
---

## Statement

Let $I$ be an interval, let $f \colon I \to \mathbb{R}$ be continuous and differentiable at each interior point of $I$, and let $K \ge 0$.
If $|f'(x)| \le K$ for each interior point $x$ of $I$, then $f$ is [[Lipschitz|0QNVQ4VD9T]] with constant $K$.

## Remarks

The [[mean value theorem|0BARQY52N5]] gives $|f(y) - f(x)| = |f'(c)| \, |y - x| \le K |y - x|$.
For example, $\sin$ is Lipschitz with constant $1$ on $\mathbb{R}$.
Mathlib states a form for convex sets as `Convex.lipschitzOnWith_of_nnnorm_deriv_le`.

## Explanations

### L1 human

If the slope of the graph never exceeds $K$ in size, no chord can be steeper than $K$.