Lebesgue Outer Measure on the Real Line

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $\mathbb{R}$ and its order be as in The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (ii), $[0,\infty]$ and $[-\infty,\infty]$ as in The Extended Real Line, Its Order, and [0,∞] (ii), the order $\le$ of $[-\infty,\infty]$ as in The Extended Real Line, Its Order, and [0,∞] (iii), and let open intervals $(a,b)$, sequences, sums of sequences in $[0,\infty]$, unions of families, infima formed in $[-\infty,\infty]$ and the power set $\mathcal{P}(\mathbb{R})$ be as there.

(i) For $A\subseteq\mathbb{R}$, a cover of $A$ by open intervals is a pair of sequences $(a_{m})$ and $(b_{m})$ in $\mathbb{R}$ with $a_{m}\le b_{m}$ for every $m\in\mathbb{N}$ and

$$A\subseteq\bigcup_{m\in\mathbb{N}}(a_{m},b_{m}),$$

the union of the sequence $m\mapsto(a_{m},b_{m})$ in $\mathcal{P}(\mathbb{R})$ given by Intervals of the Real Line as Defined Set Symbols, Typed Terms and Values of Maps (iii); by Indexed Families of Sets and Their Union, Intersection and Product (ii), this inclusion says that every $x\in A$ lies in $(a_{m},b_{m})$ for some $m\in\mathbb{N}$. Its total length is the sum $\sum_{m\in\mathbb{N}}(b_{m}-a_{m})$ in $[0,\infty]$ of the real numbers $b_{m}-a_{m}\ge0$. $\mathcal{C}(A)$ is the set of the total lengths of the covers of $A$, a subset of $[0,\infty]$ by Total Lengths of Covers by Open Intervals: the Set of Them and the Map of Their Infima (i), so that $t\in\mathcal{C}(A)$ if and only if $t$ is the total length of a cover of $A$.

(ii) The Lebesgue outer measure on $\mathbb{R}$ is the map $\lambda^{*}:\mathcal{P}(\mathbb{R})\to[0,\infty]$ with

$$\lambda^{*}(A)=\inf\mathcal{C}(A)\quad\text{for every }A\subseteq\mathbb{R},$$

which exists and is unique by Total Lengths of Covers by Open Intervals: the Set of Them and the Map of Their Infima (ii); $\lambda^{*}(A)$ is the Lebesgue outer measure of $A$.