ThmDex – An index of mathematical definitions, results, and conjectures.
P2722
Result R981: Countably infinite measurable cover has measurable subcover shows that there exists measurable, disjoint sets $F_0, F_1, F_2, \ldots \in \mathcal{F}$ such that $F_n \subseteq E_n$ for every $n \in \mathbb{N}$ and that $\bigcup_{n \in \mathbb{N}} E_n = \bigcup_{n \in \mathbb{N}} F_n$. As a consequence, result R975: Isotonicity of unsigned basic measure shows that $\mu(F_n) \subseteq \mu(E_n)$ for every $n \in \mathbb{N}$. Thus, applying disjoint additivity of $\mu$ and result R3651: Isotonicity of unsigned basic series, we have \begin{equation} \mu \left( \bigcup_{n \in \mathbb{N}} E_n \right) = \mu \left( \bigcup_{n \in \mathbb{N}} F_n \right) = \sum_{n \in \mathbb{N}} \mu(F_n) \leq \sum_{n \in \mathbb{N}} \mu(E_n) \end{equation} $\square$