Lebesgue Measure on the Real Line

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $\mathcal{P}(\mathbb{R})$ be the power set of $\mathbb{R}$, let $[0,\infty]$ be as in The Extended Real Line, Its Order, and [0,∞] (ii), and let $\lambda^{*}:\mathcal{P}(\mathbb{R})\to[0,\infty]$ be the Lebesgue outer measure on $\mathbb{R}$. Let $\mathcal{B}(\mathbb{R})$ be the Borel $\sigma$-algebra of $\mathbb{R}$. It is a $\sigma$-algebra on $\mathbb{R}$ by Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (iii), hence a subset of $\mathcal{P}(\mathbb{R})$ by σ-Algebra and Measurable Space (i).

(i) Lebesgue measure on $\mathbb{R}$ is the restriction

$$\lambda=\lambda^{*}|_{\mathcal{B}(\mathbb{R})}$$

of $\lambda^{*}$ to $\mathcal{B}(\mathbb{R})$. By Domains and Restrictions of Maps (ii) and Domains and Restrictions of Maps (iii), $\lambda$ is a map $\lambda:\mathcal{B}(\mathbb{R})\to[0,\infty]$ with $\lambda(B)=\lambda^{*}(B)$ for every $B\in\mathcal{B}(\mathbb{R})$.