Outer Measure

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $X$ be a set and let $\mathcal{P}(X)$ be its power set, whose elements are exactly the subsets of $X$. Let $\infty$, $[0,\infty]$ and the order $\le$ be as in The Extended Real Line, Its Order, and [0,∞] (i), The Extended Real Line, Its Order, and [0,∞] (ii) and The Extended Real Line, Its Order, and [0,∞] (iii), and let $0$ be the zero of $\mathbb{R}$, an element of $[0,\infty]$ by The Extended Real Line, Its Order, and [0,∞] (ii). For a sequence $(a_{m})$ in $[0,\infty]$, $\sum_{m\in\mathbb{N}}a_{m}$ is its sum. For a sequence $(A_{m})$ in $\mathcal{P}(X)$, $\bigcup_{m\in\mathbb{N}}A_{m}$ is the union of $(A_{m})$ as a family indexed by $\mathbb{N}$; it is a set by The Union and Product of a Family of Sets Indexed by a Set, and the Intersection of a Family with an Inhabited Index Class, Are Sets (i), and it is a subset of $X$, since by Indexed Families of Sets and Their Union, Intersection and Product (ii) each of its elements lies in some $A_{m}$, a subset of $X$; so $\bigcup_{m\in\mathbb{N}}A_{m}\in\mathcal{P}(X)$. The empty set $\emptyset$ is a set with no element, so it is a subset of $X$ by Subclasses and Subsets (i), and $\emptyset\in\mathcal{P}(X)$.

(i) An outer measure on $X$ is a map $\mu^{*}:\mathcal{P}(X)\to[0,\infty]$ such that $\mu^{*}(\emptyset)=0$; $\mu^{*}(A)\le\mu^{*}(B)$ for all subsets $A$ and $B$ of $X$ with $A\subseteq B$ (monotonicity); and

$$\mu^{*}\Bigl(\bigcup_{m\in\mathbb{N}}A_{m}\Bigr)\le\sum_{m\in\mathbb{N}}\mu^{*}(A_{m})$$

for every sequence $(A_{m})$ in $\mathcal{P}(X)$ (countable subadditivity), the right-hand side being the sum of the sequence $m\mapsto\mu^{*}(A_{m})$, whose terms lie in $[0,\infty]$ as $\mu^{*}$ takes its values there.