---
tag: 0EDH403M21
kind: statement
role: theorem
name: Existence of the infimum
msc: [26A03]
uses: [0AXWET80YW, 04KFTA34C5]
sources:
  - url: https://en.wikipedia.org/wiki/Least-upper-bound_property
    locator: Statement for real numbers
---

## Statement

Let $S$ be a nonempty subset of the real numbers that is [[bounded below|0B5H2V4JW8]].
Then $S$ has an [[infimum|04KFTA34C5]] in $\mathbb{R}$.

## Remarks

Proof: the set $-S = \{-s : s \in S\}$ is nonempty and bounded above. By the [[completeness axiom|0AXWET80YW]], it has a supremum $b$. Then $-b$ is the infimum of $S$.
Another proof: the set of lower bounds of $S$ is nonempty and bounded above by each element of $S$, and its supremum is $\inf S$.

## Explanations

### L1 human

If a set of real numbers has a floor, then it has a highest floor.
This follows from the completeness axiom by a reflection of the number line through $0$, which turns floors into ceilings.