Conventions: $\sup \mathrm{\varnothing }$, unbounded sets, and the extended reals

Many texts, especially in measure theory, lattice theory and optimisation, work in the extended real line $\bar{\mathbb{R}}=\mathbb{R}\cup \{-\mathrm{\infty },+\mathrm{\infty }\}$ and adopt the conventions

$\sup \mathrm{\varnothing }=-\mathrm{\infty },\inf \mathrm{\varnothing }=+\mathrm{\infty },\sup S=+\mathrm{\infty }\text{ for }S\text{ not bounded above},\inf S=-\mathrm{\infty }\text{ for }S\text{ not bounded below}\mathrm{.}$

With those conventions in force, every subset of $\mathbb{R}$ has a supremum and an infimum in $\bar{\mathbb{R}}$, and the two exceptional cases recorded in FALSE: every subset of $\mathbb{R}$ has a supremum disappear. The conventions are consistent and often convenient. The value $\sup \mathrm{\varnothing }=-\mathrm{\infty }$ is not arbitrary: it is forced by monotonicity under inclusion together with $\sup \{x\}=x$, since $\mathrm{\varnothing }\subseteq \{x\}$ then gives $\sup \mathrm{\varnothing }\le x$ for every real $x$, and $-\mathrm{\infty }$ is the only element of $\bar{\mathbb{R}}$ below every real. (Monotonicity together with $\sup \mathbb{R}=+\mathrm{\infty }$ forces nothing here: it only gives $\sup \mathrm{\varnothing }\le +\mathrm{\infty }$.) The convention also makes $\sup (S\cup T)=\max \{\sup S,\sup T\}$ hold without side conditions.

This library does not adopt them. Two reasons, both about keeping the foundations honest.

• $\pm \mathrm{\infty }$ are not elements of $\mathbb{R}$. The library's $\mathbb{R}$ is the complete ordered field (Complete ordered field (least-upper-bound property)), and $\bar{\mathbb{R}}$ is not a field: $+\mathrm{\infty }$ has no additive inverse, and the expressions $(+\mathrm{\infty })+(-\mathrm{\infty })$ and $0\cdot (+\mathrm{\infty })$ have no definition that keeps the field axioms. Writing $\sup S=+\mathrm{\infty }$ silently moves the discussion into a different structure, and every subsequent algebraic step then needs its own justification.
• Suppressed hypotheses become invisible errors. If $\sup S$ is always defined, a statement such as "$\sup (S+T)=\sup S+\sup T$" appears to be unconditional, and the cases where it degenerates are hidden inside the arithmetic of $\pm \mathrm{\infty }$ rather than shown in the hypotheses.

Accordingly, in this library:

• $\sup S$ and $\inf S$ denote real numbers, and the notation is used only after existence has been established. Existence comes from the least-upper-bound property (Complete ordered field (least-upper-bound property)) and its dual (Every nonempty set bounded below has an infimum), each of which requires the set to be nonempty and bounded on the relevant side.
• No supremum or infimum is written down before its existence has been established, and every statement that establishes existence says explicitly what it assumes. The nonempty and bounded clauses in Epsilon characterisation of the supremum, Epsilon characterisation of the infimum, Monotonicity of the supremum under inclusion, Supremum of a translate: $\sup (a+S)=a+\sup S$, Supremum of a scalar multiple and Supremum of a sumset: $\sup (S+T)=\sup S+\sup T$ are load bearing, not decoration. Where some other hypothesis does that work it is named instead of being suppressed: The supremum is attained exactly when a maximum exists obtains existence from a maximum rather than from a boundedness clause, and Suprema and infima are unique, which asserts no existence at all, needs neither clause.
• $\sup \mathrm{\varnothing }$ and $\inf \mathrm{\varnothing }$ are simply undefined (Greatest lower bound (infimum), FALSE: every subset of $\mathbb{R}$ has a supremum).

A reader coming from a source that uses the extended-real conventions should therefore expect the statements here to look more heavily qualified than the ones they are used to. The mathematics is the same; the difference is where the case analysis is written down. The extended real line is introduced explicitly in The extended real line $\bar{\mathbb{R}}=\mathbb{R}\cup \{-\mathrm{\infty },+\mathrm{\infty }\}$, its order, and the arithmetic that is left undefined ↗ for later limsup and liminf arguments, with its order and partial arithmetic kept separate from $\mathbb{R}$.