Greatest lower bound (infimum)

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

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

Written out in one line:

$\mathrm{\ell }\text{ is an infimum of }S⟺[(\mathrm{\forall }s\in S)\mathrm{\ell }\le s]\text{ and }[(\mathrm{\forall }{\mathrm{\ell }}^{\mathrm{\prime }}\in \mathbb{R})((\mathrm{\forall }s\in S){\mathrm{\ell }}^{\mathrm{\prime }}\le s)\Rightarrow {\mathrm{\ell }}^{\mathrm{\prime }}\le \mathrm{\ell }]\mathrm{.}$

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: $\mathrm{\ell }=\inf S$ exactly when $\mathrm{\ell }$ is a lower bound that cannot be raised by any positive amount without losing that property.