Proof of Properties of Lebesgue Outer Measure on the Real Line

For sequences $a=(a_{m})$ and $b=(b_{m})$ in $\mathbb{R}$ with $a_{m}\le b_{m}$ for every $m\in\mathbb{N}$ write $\ell(a,b)=\sum_{m\in\mathbb{N}}(b_{m}-a_{m})\in[0,\infty]$. For $E\subseteq\mathbb{R}$, covers $(a,b)$ of $E$, their total lengths $\ell(a,b)$ and the set $\mathcal{C}(E)$ of these are as in Lebesgue Outer Measure on the Real Line (i), by which $(a,b)$ is a cover of $E$ exactly when $a_{m}\le b_{m}$ for every $m\in\mathbb{N}$ and every $x\in E$ lies in $(a_{m},b_{m})$ for some $m\in\mathbb{N}$; and $\lambda^{*}(E)=\inf\mathcal{C}(E)$ by Lebesgue Outer Measure on the Real Line (ii). A real number $u\ge0$ is an element of $[0,\infty]$; sums and products in $[0,\infty]$ of such numbers are their real sums and products (Addition and Multiplication on [0,∞] (i) and Addition and Multiplication on [0,∞] (ii)), and on elements of $\mathbb{R}$ (The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (ii)) the order of $[-\infty,\infty]$ is that of $\mathbb{R}$, a total order on $[-\infty,\infty]$ (Order and Suprema in the Extended Real Line (i)). These identifications are used throughout.

Step 1: bounds from covers. Let $E\subseteq\mathbb{R}$. As $\lambda^{*}(E)$ is the greatest lower bound of $\mathcal{C}(E)$ in $[-\infty,\infty]$ (Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv)): (a) $\lambda^{*}(E)\le\ell(a,b)$ for every cover $(a,b)$ of $E$; (b) if $t\in[-\infty,\infty]$ and $t\le\ell(a,b)$ for every cover $(a,b)$ of $E$, then $t$ is a lower bound of $\mathcal{C}(E)$, so $t\le\lambda^{*}(E)$. (c) If $t\in[-\infty,\infty]$ and $\lambda^{*}(E)<t$, then there is a cover $(a,b)$ of $E$ with $\ell(a,b)<t$, by Order and Suprema in the Extended Real Line (x).

Step 2: an $\varepsilon$-principle. Let $x\in[0,\infty]$ and $y\in\mathbb{R}$ with $0\le y$, and suppose $x\le y+\varepsilon$ for every $\varepsilon\in\mathbb{R}$ with $\varepsilon>0$. Then $x\le y$. Indeed, $x\le y+1<\infty$, so $x\in\mathbb{R}$ by Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (iii). If $y<x$, then $\varepsilon=(x-y)/2>0$ and $x\le y+(x-y)/2<y+(x-y)=x$ by Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares (vii), which is impossible; so $x\le y$, the order being total.

Step 3: the lengths $\varepsilon/2^{m}$. Let $\varepsilon\in\mathbb{R}$ with $\varepsilon>0$, let $r=1/2$ and $\delta_{m}=\varepsilon r^{m}$ for $m\in\mathbb{N}$. Then $\delta_{m}\in\mathbb{R}$ and $\delta_{m}>0$ for every $m$, and $\sum_{m\in\mathbb{N}}\delta_{m}=\varepsilon$. Indeed, $0<r<1$ by Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares (vii), so $|r|<1$ and $r^{m}>0$ (Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (vi)), whence $\delta_{m}>0$ by Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares (iv). The real series $\sum_{k=1}^{\infty}r^{k}$ converges with sum $r/(1-r)=1$, as $1-r=r$, by Series of Real Numbers with Nonnegative Terms, Comparison, Absolute Convergence and the Geometric Series (v); so $\sum_{k\in\mathbb{N}}r^{k}=1$ by Sums of Sequences in [0,∞]: Real Series, Linearity, Comparison, Rearrangement, Double Series and Monotone Convergence (vi), and $\sum_{m\in\mathbb{N}}\delta_{m}=\varepsilon\sum_{m\in\mathbb{N}}r^{m}=\varepsilon$ by Sums of Sequences in [0,∞]: Real Series, Linearity, Comparison, Rearrangement, Double Series and Monotone Convergence (ix).

Step 4: combining covers. (W) Let $w:\mathbb{N}\times\mathbb{N}\to[0,\infty]$ be a map. For $m\in\mathbb{N}$, Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v), with $\mathbb{N}$ and $[0,\infty]$ for its $A$ and $B$, $m$ for its $v_{1}$, the guard $m\in\mathbb{N}$ for its $\gamma$, $n$ for its $u$ and the value $w(m,n)$ of $w$ at $(m,n)$, a defined set symbol used properly and lying in $[0,\infty]$, for its $t(u,v_{1})$, gives a predicative formula $\theta(h,m)$ whose only solution $h$ is the map $n\mapsto w(m,n)$ from $\mathbb{N}$ to $[0,\infty]$. So this map is a defined set symbol with argument $m$, used properly at every $m\in\mathbb{N}$, and an element of the set $[0,\infty]^{\mathbb{N}}$ of sequences in $[0,\infty]$ (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i) and The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (ii)); and Maps and Relations Given by Formulas (i), applied to $\mathbb{N}$, $[0,\infty]^{\mathbb{N}}$ and this expression, gives the map $m\mapsto(n\mapsto w(m,n))$ from $\mathbb{N}$ to $[0,\infty]^{\mathbb{N}}$. By Sums of Sequences in [0,∞] as Typed Terms and as a Map (ii), applied to $D=\mathbb{N}$ and this map, the inner sums form a sequence $m\mapsto\sum_{n\in\mathbb{N}}w(m,n)$ in $[0,\infty]$.

Let $E\subseteq\mathbb{R}$ and let $\alpha,\beta:\mathbb{N}\times\mathbb{N}\to\mathbb{R}$ be maps with $\alpha(m,n)\le\beta(m,n)$ for all $m,n\in\mathbb{N}$, such that for every $x\in E$ there are $m,n\in\mathbb{N}$ with $\alpha(m,n)<x<\beta(m,n)$. Then

$$\lambda^{*}(E)\le\sum_{m\in\mathbb{N}}\sum_{n\in\mathbb{N}}\bigl(\beta(m,n)-\alpha(m,n)\bigr).$$

Here $w(m,n)=\beta(m,n)-\alpha(m,n)$ is a real number with $0\le w(m,n)$, so it lies in $[0,\infty]$, and $w:\mathbb{N}\times\mathbb{N}\to[0,\infty]$ is a map by Maps and Relations Given by Formulas (ii); the inner sums form the sequence $m\mapsto\sum_{n\in\mathbb{N}}w(m,n)$ in $[0,\infty]$ of (W). To prove the inequality, let $\tau:\mathbb{N}\to\mathbb{N}\times\mathbb{N}$ be a bijection, which exists by Countable Sets: a Bijection from ℕ onto ℕ×ℕ, Finite Sets, Subsets, Surjective Images, Images, Products, and the Integers and Rationals (ii). The sequences $e_{k}=\alpha(\tau(k))$ and $f_{k}=\beta(\tau(k))$ satisfy $e_{k}\le f_{k}$, and $(e,f)$ is a cover of $E$: for $x\in E$ take $m,n$ as above and $k\in\mathbb{N}$ with $\tau(k)=(m,n)$; then $e_{k}<x<f_{k}$. By Step 1(a) and Sums of Sequences in [0,∞]: Real Series, Linearity, Comparison, Rearrangement, Double Series and Monotone Convergence (xiii),

$$\lambda^{*}(E)\le\ell(e,f)=\sum_{k\in\mathbb{N}}w(\tau(k))=\sum_{m\in\mathbb{N}}\sum_{n\in\mathbb{N}}w(m,n).$$

Proof of (i). The constant sequences $a_{m}=b_{m}=0$ form a cover of $\emptyset$, and $\ell(a,b)=\sum_{m\in\mathbb{N}}0=0$ by Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (iv). So $\lambda^{*}(\emptyset)\le0$ by Step 1(a), and $\lambda^{*}(\emptyset)=0$ by Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (i).

Proof of (ii). Let $A\subseteq B$. Every cover of $B$ is a cover of $A$, so $\lambda^{*}(A)\le\ell(a,b)$ for every cover $(a,b)$ of $B$ by Step 1(a), and $\lambda^{*}(A)\le\lambda^{*}(B)$ by Step 1(b).

Proof of (iii). If $\lambda^{*}(A)=\infty$ or $\lambda^{*}(B)=\infty$, then $\lambda^{*}(A)+\lambda^{*}(B)=\infty$ (Addition and Multiplication on [0,∞] (i)), and the claim holds as $\infty$ is the greatest element of $[-\infty,\infty]$ (Order and Suprema in the Extended Real Line (ii)). Otherwise $\lambda^{*}(A)$ and $\lambda^{*}(B)$ are real by Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (ii). Fix first $\varepsilon\in\mathbb{R}$ with $\varepsilon>0$; then $\varepsilon/2>0$ and $\varepsilon/2+\varepsilon/2=\varepsilon$ (Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares (vii)). As $\lambda^{*}(A)<\lambda^{*}(A)+\varepsilon/2$, Step 1(c) gives a cover $(a,b)$ of $A$ with $\ell(a,b)<\lambda^{*}(A)+\varepsilon/2$; likewise fix a cover $(c,d)$ of $B$ with $\ell(c,d)<\lambda^{*}(B)+\varepsilon/2$. Only these two covers are taken. Let $\alpha,\beta:\mathbb{N}\times\mathbb{N}\to\mathbb{R}$ be the maps with $\alpha(1,n)=a_{n}$, $\alpha(2,n)=c_{n}$, $\beta(1,n)=b_{n}$, $\beta(2,n)=d_{n}$, and $\alpha(m,n)=\beta(m,n)=0$ for $m\notin\{1,2\}$ (Maps Defined by Cases (i), applied twice for each map). Then $\alpha\le\beta$, and every $x\in A\cup B$ lies in $(a_{n},b_{n})$ or in $(c_{n},d_{n})$ for some $n$, so Step 4 applies to $E=A\cup B$. For $u_{m}=\sum_{n\in\mathbb{N}}(\beta(m,n)-\alpha(m,n))$ we have $u_{1}=\ell(a,b)$, $u_{2}=\ell(c,d)$, and $u_{m}=0$ for $m>2$ by Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (iv); so $\sum_{m\in\mathbb{N}}u_{m}=u_{1}+u_{2}$ by Sums of Sequences in [0,∞]: Real Series, Linearity, Comparison, Rearrangement, Double Series and Monotone Convergence (vii), Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (vii) and Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (i), which apply as $+$ on $[0,\infty]$ is associative and commutative with neutral element $0$ (Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (i)); here $m\mapsto u_{m}$ is the sequence in $[0,\infty]$ of (W) for the map $w$ of Step 4, $w(m,n)=\beta(m,n)-\alpha(m,n)$. Hence, by Step 4 and Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (iv),

$$\lambda^{*}(A\cup B)\le\ell(a,b)+\ell(c,d)\le\bigl(\lambda^{*}(A)+\lambda^{*}(B)\bigr)+\varepsilon,$$

all terms on the right being real. As $\varepsilon>0$ was arbitrary, Step 2 gives the claim.

Proof of (iv). The intervals $[p,q]$. Let $p,q\in\mathbb{R}$ with $p\le q$; we show $\lambda^{*}([p,q])=q-p$. For every cover $(a,b)$ of $[p,q]$, $q-p\le\ell(a,b)$ by A Closed Interval Covered by Open Intervals Is No Longer than Their Total Length (ii); so $q-p\le\lambda^{*}([p,q])$ by Step 1(b). Conversely, let $\varepsilon\in\mathbb{R}$ with $\varepsilon>0$, and let $(a_{m})$ and $(b_{m})$ be the sequences with $a_{1}=p-\varepsilon/2$, $b_{1}=q+\varepsilon/2$ and $a_{m}=b_{m}=0$ for $m\neq1$ (Maps Defined by Cases (i)). Then $a_{m}\le b_{m}$ for every $m$, every $x\in[p,q]$ satisfies $a_{1}<x<b_{1}$, and $b_{m}-a_{m}=0$ for $m>1$; so $(a,b)$ is a cover of $[p,q]$ with $\ell(a,b)=b_{1}-a_{1}=(q-p)+\varepsilon$ by Sums of Sequences in [0,∞]: Real Series, Linearity, Comparison, Rearrangement, Double Series and Monotone Convergence (vii) and Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (i), which apply as $+$ on $[0,\infty]$ is associative and commutative with neutral element $0$ (Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (i)). By Step 1(a), $\lambda^{*}([p,q])\le(q-p)+\varepsilon$, and by Step 2, $\lambda^{*}([p,q])\le q-p$. So $\lambda^{*}([p,q])=q-p$, the order being antisymmetric. In particular $\lambda^{*}([p,p])=0$ for every $p\in\mathbb{R}$.

The four intervals. Let $a\le b$. Every $x\in[a,b]$ satisfies $x=a$, $x=b$ or $a<x<b$, so $[a,b]\subseteq((a,b)\cup[a,a])\cup[b,b]$. By (ii), (iii) applied twice, Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (iv) and the closed case,

$$\lambda^{*}([a,b])\le\lambda^{*}((a,b)\cup[a,a])+\lambda^{*}([b,b])\le\bigl(\lambda^{*}((a,b))+0\bigr)+0=\lambda^{*}((a,b)),$$

$0$ being neutral (Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (i)). Let $I$ be one of $(a,b)$, $[a,b]$, $[a,b)$ and $(a,b]$. Then $(a,b)\subseteq I\subseteq[a,b]$, so by (ii) and the closed case

$$b-a=\lambda^{*}([a,b])\le\lambda^{*}((a,b))\le\lambda^{*}(I)\le\lambda^{*}([a,b])=b-a,$$

and $\lambda^{*}(I)=b-a$.

Proof of (v). Let $c\in\mathbb{R}$; then $A\cap(c,\infty)=\{x\in A:c<x\}$ and $A\setminus(c,\infty)=\{x\in A:x\le c\}$. Maxima and minima of two real numbers are as in The Maximum and Minimum of Two Elements of a Total Order (i), for the total order of $\mathbb{R}$.

First let $(a,b)$ be a cover of $A$ and $\varepsilon\in\mathbb{R}$ with $\varepsilon>0$, and let $(\delta_{m})$ be as in Step 3 for this $\varepsilon$. Define, for $m\in\mathbb{N}$,

$$a'_{m}=\max\{a_{m},c\},\quad b'_{m}=\max\{b_{m},c\},\quad a''_{m}=\min\{a_{m},c\},\quad b''_{m}=\min\{b_{m},c\}+\delta_{m}.$$

As $a_{m}\le b_{m}\le b'_{m}$ and $c\le b'_{m}$, The Maximum and Minimum of Two Elements of a Total Order (iii) and The Maximum and Minimum of Two Elements of a Total Order (iv) give $a'_{m}\le b'_{m}$; as $a''_{m}\le a_{m}\le b_{m}$ and $a''_{m}\le c$ by The Maximum and Minimum of Two Elements of a Total Order (iii), The Maximum and Minimum of Two Elements of a Total Order (v) gives $a''_{m}\le\min\{b_{m},c\}<b''_{m}$.

$(a',b')$ is a cover of $A\cap(c,\infty)$: let $x\in A$ with $c<x$, and $m$ with $a_{m}<x<b_{m}$. Then $a'_{m}$ is $a_{m}$ or $c$ (The Maximum and Minimum of Two Elements of a Total Order (ii)), so $a'_{m}<x$; and $x<b_{m}\le b'_{m}$.

$(a'',b'')$ is a cover of $A\setminus(c,\infty)$: let $x\in A$ with $x\le c$, and $m$ with $a_{m}<x<b_{m}$. Then $a''_{m}\le a_{m}<x$, and $x\le\min\{b_{m},c\}<b''_{m}$ by The Maximum and Minimum of Two Elements of a Total Order (v).

By The Maximum and Minimum of Two Elements of an Ordered Field: Sum, Difference and Absolute Value (i), $b'_{m}+\min\{b_{m},c\}=b_{m}+c$ and $a'_{m}+a''_{m}=a_{m}+c$, so

$$(b'_{m}-a'_{m})+(b''_{m}-a''_{m})=(b_{m}+c)-(a_{m}+c)+\delta_{m}=(b_{m}-a_{m})+\delta_{m}.$$

Hence, by Sums of Sequences in [0,∞]: Real Series, Linearity, Comparison, Rearrangement, Double Series and Monotone Convergence (viii) (twice) and Step 3,

$$\ell(a',b')+\ell(a'',b'')=\sum_{m\in\mathbb{N}}\bigl((b_{m}-a_{m})+\delta_{m}\bigr)=\ell(a,b)+\varepsilon,$$

and by Step 1(a) and Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (iv), applied twice,

$$\lambda^{*}(A\cap(c,\infty))+\lambda^{*}(A\setminus(c,\infty))\le\ell(a,b)+\varepsilon.\tag{$\ast$}$$

Now, if $\lambda^{*}(A)=\infty$ the claim holds by Order and Suprema in the Extended Real Line (ii). Otherwise $\lambda^{*}(A)\in\mathbb{R}$ by Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (ii). Fix first $\varepsilon\in\mathbb{R}$ with $\varepsilon>0$; then Step 1(c), as $\lambda^{*}(A)<\lambda^{*}(A)+\varepsilon/2$, gives one cover $(a,b)$ of $A$ with $\ell(a,b)<\lambda^{*}(A)+\varepsilon/2$, and $(\ast)$ for this cover and $\varepsilon/2$ gives

$$\lambda^{*}(A\cap(c,\infty))+\lambda^{*}(A\setminus(c,\infty))\le\lambda^{*}(A)+\varepsilon.$$

No choice is made beyond this one cover: the covers $(a',b')$ and $(a'',b'')$ are given by expressions in it. As $\varepsilon>0$ was arbitrary, Step 2 gives the claim.

Proof of (vi). Let $(A_{m})$ be a sequence in $\mathcal{P}(\mathbb{R})$, let $E=\bigcup_{m\in\mathbb{N}}A_{m}$, so that $x\in E$ if and only if $x\in A_{m}$ for some $m\in\mathbb{N}$ (Indexed Families of Sets and Their Union, Intersection and Product (ii)), and let $\sigma=\sum_{m\in\mathbb{N}}\lambda^{*}(A_{m})$. If $\sigma=\infty$, the claim holds by Order and Suprema in the Extended Real Line (ii). Otherwise, for every $m$, $\lambda^{*}(A_{m})\le\sigma<\infty$ by Sums of Sequences in [0,∞]: Real Series, Linearity, Comparison, Rearrangement, Double Series and Monotone Convergence (iii), so $\lambda^{*}(A_{m})\in\mathbb{R}$ by Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (iii).

Fix first $\varepsilon\in\mathbb{R}$ with $\varepsilon>0$, and let $(\delta_{m})$ be as in Step 3. The set $\mathbb{R}^{\mathbb{N}}$ of sequences in $\mathbb{R}$ is a set by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (ii), and so is $\Omega=\mathbb{R}^{\mathbb{N}}\times\mathbb{R}^{\mathbb{N}}$, by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii). For $m\in\mathbb{N}$ let

$$K_{m}=\{(a,b)\in\Omega:(a,b)\text{ is a cover of }A_{m}\text{ and }\ell(a,b)<\lambda^{*}(A_{m})+\delta_{m}\},$$

a subset of $\Omega$, hence an element of the set $\mathcal{P}(\Omega)$ (The Union Set and the Power Set of a Set (ii)); its condition, on $m$ and an element $p$ of $\Omega$, is expressed by a predicative formula, with the sequences $(A_{m})$ and $(\delta_{m})$, the map $\lambda^{*}$, $\Omega$, the strict relation $<$ of $[-\infty,\infty]$ (Partial and Total Orders on a Set and the Associated Strict Relation (iii)) and $\mathbb{N}$, $\mathbb{R}$, $\mathbb{R}^{\mathbb{N}}$, the order, the operations $+$ and $\cdot$ and the elements $0$ and $1$ of $\mathbb{R}$, $\mathcal{P}(\mathbb{R})$, $[-\infty,\infty]$ and its order, $[0,\infty]$, $[0,\infty]^{\mathbb{N}}$, the sum on $[0,\infty]$, and the order and the addition of $\mathbb{N}_{0}$ as parameters. The class variables for these parameters are chosen pairwise distinct whenever their values differ: in particular the order of $\mathbb{R}$ and the order of $[-\infty,\infty]$ are different variables, although Intervals of the Real Line as Defined Set Symbols, Typed Terms and Values of Maps (ii) and Sums of Sequences in [0,∞] as Typed Terms and as a Map (i) both write $L$ for theirs, and likewise $+$ of $\mathbb{R}$ and the sum $+$ on $[0,\infty]$.

Namely, the condition is $\exists a\,\exists b\,(p=(a,b)\wedge\kappa)$, with $p=(a,b)$ in the predicative form of Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (v), and $\kappa$ formed as follows under one guard $G$ on $a$, $b$ and $m$ throughout: $G$ is $\gamma\wedge m\in\mathbb{N}$, where $\gamma$ is $a\in\mathbb{R}^{\mathbb{N}}\wedge b\in\mathbb{R}^{\mathbb{N}}\wedge\forall n\,(n\in\mathbb{N}\Rightarrow\exists u\,\exists v\,((n,u)\in a\wedge(n,v)\in b\wedge u\le v))$; $\gamma$ and $G$ are predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i). As $(n,z)\in a$ if and only if $z=a_{n}$ for a map $a$ with domain $\mathbb{N}$ and $n\in\mathbb{N}$ (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x)), and likewise for $b$, $G$ states that $a$ and $b$ are sequences in $\mathbb{R}$ with $a_{n}\le b_{n}$ for every $n\in\mathbb{N}$, and that $m\in\mathbb{N}$. For the index terms we use the guard $G\wedge n\in\mathbb{N}$ on $a$, $b$, $m$ and $n$: under it $a_{n}$ and $b_{n}$ are terms of type $\mathbb{R}$ (Terms and Typed Terms under a Guard (ii)), $b_{n}-a_{n}$ is one of type $[0,\infty]$, its equation being expressed with the formula of Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (iv), and $(a_{n},b_{n})$ is one of type $\mathcal{P}(\mathbb{R})$ by Intervals of the Real Line as Defined Set Symbols, Typed Terms and Values of Maps (ii). Thus $b_{n}-a_{n}$ is an expression built from the defined set symbols $a_{n}$, $b_{n}$ and $u-v$, used properly and lying in $[0,\infty]$ for all $a$, $b$ and $m$ satisfying $G$ and every $n\in\mathbb{N}$. So Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v), with $\mathbb{N}$ and $[0,\infty]$ for its $A$ and $B$, $a$, $b$ and $m$ for its $v_{1}$, $v_{2}$ and $v_{3}$, $G$ for its $\gamma$, $n$ for its $u$ and $b_{n}-a_{n}$ for its $t(u,v_{1},v_{2},v_{3})$, gives a predicative formula $\theta(h,a,b,m)$ such that, for all $a$, $b$ and $m$ satisfying $G$, the only set $h$ with $\theta(h,a,b,m)$ is the map $n\mapsto b_{n}-a_{n}$ from $\mathbb{N}$ to $[0,\infty]$, an element of $[0,\infty]^{\mathbb{N}}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i). Hence $G\wedge\theta(h,a,b,m)$ expresses $G\wedge h=(n\mapsto b_{n}-a_{n})$, and $n\mapsto b_{n}-a_{n}$ is a term of type $[0,\infty]^{\mathbb{N}}$ under $G$ (Terms and Typed Terms under a Guard (ii)); and Sums of Sequences in [0,∞] as Typed Terms and as a Map (i), with $G$ for its $\gamma$ and this term for its $a$, makes $\ell(a,b)$ a term of type $[0,\infty]$ under $G$. "Every $x\in A_{m}$ lies in $(a_{n},b_{n})$ for some $n\in\mathbb{N}$" is expressed by $\forall x\,(\exists y\,(y=A_{m}\wedge x\in y)\Rightarrow\exists n\,(n\in\mathbb{N}\wedge\exists z\,(z=(a_{n},b_{n})\wedge x\in z)))$, the equations $y=A_{m}$ and $z=(a_{n},b_{n})$ having predicative forms, under $G$ and under $G\wedge n\in\mathbb{N}$ respectively, by Terms and Typed Terms under a Guard (iv). Here $m$ is a term of type $\mathbb{N}$ under $G$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (i), so $A_{m}$, the value of $(A_{m})$ at $m$, is a term of type $\mathcal{P}(\mathbb{R})$ under $G$ and $\lambda^{*}(A_{m})$ one of type $[0,\infty]$, by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), $\lambda^{*}$ being a map from $\mathcal{P}(\mathbb{R})$ to $[0,\infty]$ (Lebesgue Outer Measure on the Real Line (ii)). As every $\delta_{n}$ is a positive real number, $(\delta_{n})$ is also a map from $\mathbb{N}$ to $[0,\infty]$ (Functions, Values of a Function, and Functions from One Class to Another (iii)), so $\delta_{m}$ is a term of type $[0,\infty]$ under $G$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii). All terms below are under $G$. Then $(\lambda^{*}(A_{m}),\delta_{m})$ is a term of type $[0,\infty]\times[0,\infty]$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iv), and $\lambda^{*}(A_{m})+\delta_{m}$, the value at it of the sum on $[0,\infty]$, a map from $[0,\infty]\times[0,\infty]$ to $[0,\infty]$ (Addition and Multiplication on [0,∞] (i) and Binary Operations on a Set (i)), is a term of type $[0,\infty]$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii). Finally $(\ell(a,b),\lambda^{*}(A_{m})+\delta_{m})$ is a term of type $[0,\infty]\times[0,\infty]$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iv), and $\ell(a,b)<\lambda^{*}(A_{m})+\delta_{m}$, which says that this pair lies in $<$, is expressed by a predicative formula by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (vi). $\kappa$ is the conjunction of the formulas obtained, and $\exists a\,\exists b\,(p=(a,b)\wedge\kappa)$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i). So $K_{m}$ is a defined set symbol used properly at every $m\in\mathbb{N}$, and Maps and Relations Given by Formulas (i), applied to $\mathbb{N}$, $\mathcal{P}(\Omega)$ and this expression, gives the map $m\mapsto K_{m}$, a family indexed by $\mathbb{N}$. Each $K_{m}$ is nonempty: $\lambda^{*}(A_{m})<\lambda^{*}(A_{m})+\delta_{m}$, so Step 1(c) gives a cover $(a,b)$ of $A_{m}$ with $\ell(a,b)<\lambda^{*}(A_{m})+\delta_{m}$, and $(a,b)\in\Omega$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i) and Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i). By Countable Choice Follows from Dependent Choice (i), applied to the set $\Omega$ and the family $(K_{m})$, there is a map $\xi:\mathbb{N}\to\Omega$ with $\xi_{m}\in K_{m}$ for every $m\in\mathbb{N}$. This is the only choice in the argument, made after $\varepsilon$ is fixed. Write $\xi_{m}=(a^{(m)},b^{(m)})$, and let $\alpha,\beta:\mathbb{N}\times\mathbb{N}\to\mathbb{R}$ be the maps $\alpha(m,n)=a^{(m)}_{n}$ and $\beta(m,n)=b^{(m)}_{n}$, which exist by Maps and Relations Given by Formulas (ii), as $a^{(m)}_{n}$ and $b^{(m)}_{n}$ are values at $n$ of the components of the value $\xi_{m}$, maps $\mathbb{N}\to\mathbb{R}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), and so lie in $\mathbb{R}$. Then $\alpha\le\beta$, as each $(a^{(m)},b^{(m)})$ is a cover, and every $x\in E$ lies in some $A_{m}$, hence in $(a^{(m)}_{n},b^{(m)}_{n})$ for some $n$, as $(a^{(m)},b^{(m)})$ is a cover of $A_{m}$. The sequence $m\mapsto\ell(a^{(m)},b^{(m)})$ in $[0,\infty]$ is given by Sums of Sequences in [0,∞] as Typed Terms and as a Map (ii), as in (W) for the map $w$ of Step 4: since $\beta(m,n)-\alpha(m,n)=b^{(m)}_{n}-a^{(m)}_{n}$ for all $m,n\in\mathbb{N}$, the $m$-th inner sum of Step 4 is $\sum_{n\in\mathbb{N}}(b^{(m)}_{n}-a^{(m)}_{n})=\ell(a^{(m)},b^{(m)})$. By Step 4, Sums of Sequences in [0,∞]: Real Series, Linearity, Comparison, Rearrangement, Double Series and Monotone Convergence (x), Sums of Sequences in [0,∞]: Real Series, Linearity, Comparison, Rearrangement, Double Series and Monotone Convergence (viii) and Step 3,

$$\lambda^{*}(E)\le\sum_{m\in\mathbb{N}}\ell\bigl(a^{(m)},b^{(m)}\bigr)\le\sum_{m\in\mathbb{N}}\bigl(\lambda^{*}(A_{m})+\delta_{m}\bigr)=\sigma+\varepsilon.$$

As $\varepsilon>0$ was arbitrary and $\sigma\in\mathbb{R}$ by Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (ii), Step 2 gives $\lambda^{*}(E)\le\sigma$.

Proof of (vii). $\lambda^{*}$ is a map from $\mathcal{P}(\mathbb{R})$ to $[0,\infty]$ by Lebesgue Outer Measure on the Real Line (ii); it satisfies $\lambda^{*}(\emptyset)=0$ by (i), is monotone by (ii), and is countably subadditive by (vi). As $\mathbb{R}$ is a set by The Real Numbers (i), these are the conditions of Outer Measure (i) for $X=\mathbb{R}$.