ThmDex – An index of mathematical definitions, results, and conjectures.
P3232
Let $\mathsf{Covers}(E)$ and $\mathsf{Covers}(F)$ each denote the set of countable coverings of $E$ and $F$, respectively, consisting of open $D$-intervals. By definition, if $\{ I_n \}_{n \in \mathbb{N}}$ is such a covering for $F$, then $F \subseteq \bigcup_{n \in \mathbb{N}} I_n$. Since $E \subseteq F$, then also $E \subseteq \bigcup_{n \in \mathbb{N}} I_n$. That is, every such covering for $F$ is also a covering for $E$. Therefore, if $\mathsf{Vol}$ denotes the D1738: Euclidean real volume function on $\mathbb{R}^D$, then we have the inclusion \begin{equation} \left\{ \sum_{n \in \mathbb{N}} \mathsf{Vol}(I_n) : \{ I_n \}_{n \in \mathbb{N}} \in \mathsf{Covers}(F) \right\} \subseteq \left\{ \sum_{n \in \mathbb{N}} \mathsf{Vol}(I_n) : \{ I_n \}_{n \in \mathbb{N}} \in \mathsf{Covers}(E) \right\} \end{equation} Now R1109: Antitonicity of infimum implies \begin{equation} \begin{split} \ell^*(F) = \inf_{\{ I_n \}_{n \in \mathbb{N}} \in \mathsf{Covers}(F)} \sum_{n \in \mathbb{N}} \mathsf{Vol}(I_n) \geq \inf_{\{ I_n \}_{n \in \mathbb{N}} \in \mathsf{Covers}(E)} \sum_{n \in \mathbb{N}} \mathsf{Vol}(I_n) = \ell^*(E) \end{split} \end{equation} This concludes the proof. $\square$