Theorem: Induced Outer Measure Restricted to Semiring is Pre-Measure

Let $\SS$ be a semiring over a set $X$.
Let $\mu: \SS \to \overline \R_{\ge 0}$ be a pre-measure on $\SS$, where $\overline \R_{\ge 0}$ denotes the set of positive extended real numbers.
Let $\mu^*: \powerset X \to \overline \R_{\ge 0}$ be the outer measure induced by $\mu$.
Then:
:$\ds \mu^*\restriction_\SS \, = \mu$
where $\restriction$ denotes restriction.

Proof:
Let $S \in \SS$.
It follows immediately from the definition of the induced outer measure that $\map {\mu^*} S \le \map \mu S$.
Therefore, it suffices to show that if $\ds \sequence {A_n}_{n \mathop = 0}^\infty$ is a countable cover for $S$, then:
:$\ds \map \mu S \le \sum_{n \mathop = 0}^\infty \map \mu {A_n}$
If the above statement is true, then it follows directly from the definition of infimum that $\map \mu S \le \map {\mu^*} S$, thus proving the theorem.
{{refactor|The structure of this proof needs to be clarified. I recommend that the induction part of it be extracted into a separately-paged lemma, structured as our usual house style.|level = medium}}
Define, for all natural numbers $n \in \N$:
:$\ds B_n = A_n \setminus A_{n - 1} \setminus \cdots \setminus A_0$
where $\setminus$ denotes set difference.
We take $B_0 = A_0$.
Using the mathematical induction, we will prove that for all natural numbers $m < n$, $B_{n, m} = A_n \setminus A_{n-1} \setminus \cdots \setminus A_{n-m}$ is the finite union of pairwise disjoint elements of $\SS$.
We take $B_{n, 0} = A_n$.
The base case $m = 0$ is trivial.
{{Disambiguate|Definition:Trivial}}
Now assume the induction hypothesis that the above statement is true for some natural number $m < n - 1$, and let $D_1, D_2, \ldots, D_N$ be pairwise disjoint elements of $\SS$ such that:
:$\ds B_{n, m} = \bigcup_{k \mathop = 1}^N D_k$
Then:
{{begin-eqn}}
{{eqn | l = B_{n, m+1}
      | r = B_{n, m} \setminus A_{n - m - 1}
}}
{{eqn | r = \paren {\bigcup_{k \mathop = 1}^N D_k} \setminus A_{n - m - 1}
}}
{{eqn | r = \bigcup_{k \mathop = 1}^N \paren {D_k \setminus A_{n - m - 1} }
      | c = by Set Difference is Right Distributive over Union
}}
{{end-eqn}}
By the definition of a semiring, for all natural numbers $k \le N$, $D_k \setminus A_{n - m - 1}$ is the finite union of pairwise disjoint elements of $\SS$.
Hence $B_{n, m+1}$ is the finite union of pairwise disjoint elements of $\SS$, completing the induction step.
Therefore, $B_{n, n-1} = B_n$ is the finite union of pairwise disjoint elements of $\SS$, as desired.
Using the above result and applying the axiom of countable choice, we can, for all $n \in \N$, choose a finite set $\FF_n$ of pairwise disjoint elements of $\SS$ for which:
:$\ds B_n = \bigcup \FF_n$
Now, $x \in S$ {{iff}} there exists an $n \in \N$ such that $x \in S \cap A_n$.
Taking the smallest such $n$, which exists because $\N$ is well-ordered, it follows that $x \notin A_0, A_1, \ldots, A_{n - 1}$, and so $x \in S \cap B_n$.
Therefore:
:$\ds S = \bigcup_{n \mathop = 0}^\infty \paren {S \cap B_n}$
Hence:
{{begin-eqn}}
{{eqn | l = \map \mu S
      | r = \map \mu {\bigcup_{n \mathop = 0}^\infty \paren {S \cap B_n} }
}}
{{eqn | r = \map \mu {\bigcup_{n \mathop = 0}^\infty \paren {S \cap \bigcup_{T \mathop \in \FF_n} T} }
      | c = by definition of $\FF_n$
}}
{{eqn | r = \map \mu {\bigcup_{n \mathop = 0}^\infty \bigcup_{T \mathop \in \FF_n} \paren {S \cap T} }
      | c = Intersection Distributes over Union
}}
{{eqn | o = \le
      | r = \sum_{n \mathop = 0}^\infty \sum_{T \mathop \in \FF_n} \map \mu {S \cap T}
      | c = countable union of finite sets is countable and {{Defof|Countably Subadditive Function}}
}}
{{eqn | o = \le
      | r = \sum_{n \mathop = 0}^\infty \sum_{T \mathop \in \FF_n} \map \mu T
      | c = {{Defof|Monotone (Measure Theory)|Monotone}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \map \mu {\bigcup \FF_n}
      | c = {{Defof|Additive Function (Measure Theory)|Additive Function}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \map \mu {B_n}
      | c = by definition of $\FF_n$
}}
{{eqn | o = \le
      | r = \sum_{n \mathop = 0}^\infty \map \mu {A_n}
      | c = Set Difference is Subset and {{Defof|Monotone (Measure Theory)|Monotone}}
}}
{{end-eqn}}
{{qed}}
{{ACC}}
Category:Outer Measures
Category:Pre-Measures
0uk9pzxpujrgcwggw351wphhg2gcpkk