---
tag: 0WS1A8E2P9
kind: statement
role: theorem
name: Extreme value theorem
msc: [26A15]
uses: [0ATVXC3NCC, 0P27W9RW0G]
sources:
  - url: https://en.wikipedia.org/wiki/Extreme_value_theorem
    locator: lead section
same_as:
  wikidata: Q752375
  wikipedia: Extreme value theorem
---

## Statement

Let $a \le b$ and let $f \colon [a, b] \to \mathbb{R}$ be [[continuous|0P27W9RW0G]].
Then there are $c, d \in [a, b]$ with $f(c) \le f(x) \le f(d)$ for all $x \in [a, b]$.

## Remarks

By the [[boundedness theorem|0ATVXC3NCC]], $M = \sup f([a, b])$ is finite. If $f(x) < M$ for all $x$, then $1/(M - f(x))$ is continuous and unbounded, which is a contradiction.
Each hypothesis is needed. The function $x$ on $[0, 1)$ has no maximum, and $x$ on $[0, \infty)$ is not bounded above.
Mathlib states it for compact sets, as `IsCompact.exists_isMinOn` and `IsCompact.exists_isMaxOn`.

## History

Bernard Bolzano proved the theorem in the 1830s. His proof stayed unpublished until 1930.

## Explanations

### L1 human

On a closed bounded interval, a continuous function has a highest value and a lowest value.
Its graph has a top point and a bottom point.