Greatest lower bound (infimum)

Let $S \subseteq \mathbb{R}$ and $\ell \in \mathbb{R}$. Then $\ell$ is a greatest lower bound, or infimum, of $S$ if both of the following hold:

• $\ell$ is a lower bound of $S$ (Lower bound, bounded below, bounded set), that is, $\ell \le s$ for every $s \in S$;
• $\ell' \le \ell$ for every lower bound $\ell'$ of $S$.

Written out in one line:

$\ell \text{ is an infimum of } S \iff \big[(\forall s \in S)\, \ell \le s\big] \text{ and } \big[(\forall \ell' \in \mathbb{R})\, \big((\forall s \in S)\, \ell' \le s\big) \Rightarrow \ell' \le \ell\big].$

An infimum, when it exists, is unique (Suprema and infima are unique ↗), so we may write $\inf S$ for it.

• This is the exact dual of the least upper bound (supremum) of Complete ordered field (least-upper-bound property): reverse every inequality and swap "least" for "greatest". The two notions are related by reflection through $0$ (Reflection through zero exchanges upper and lower bounds).
• Existence is deliberately not part of the definition. That every nonempty subset of $\mathbb{R}$ which is bounded below actually has an infimum is a theorem, Every nonempty set bounded below has an infimum, derived from the least-upper-bound property; it is not an axiom and it is not free.
• As with a supremum, an infimum need not belong to $S$; when it does, it is the minimum of $S$ (Maximum and minimum of a set).
• The usable form of the definition in later arguments is the epsilon characterisation Epsilon characterisation of the infimum: $\ell = \inf S$ exactly when $\ell$ is a lower bound that cannot be raised by any positive amount without losing that property.