Restricting a Measure to a Measurable Set

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $(X,\mathcal{F},\mu)$ be a measure space, so that $(X,\mathcal{F})$ is a measurable space and $\mu$ is a measure on it, with values in the set $[0,\infty]$ of The Extended Real Line, Its Order, and [0,∞] (ii), ordered by the order $\le$ and the relation $<$ of The Extended Real Line, Its Order, and [0,∞] (iii), and with $\infty$ the point of The Extended Real Line, Its Order, and [0,∞] (i). Let $Y\in\mathcal{F}$, and let $\mathcal{F}_{Y}=\{A\in\mathcal{F}:A\subseteq Y\}$, with $\subseteq$ the subclass relation and intersections of classes those of The Boolean Operations on Classes, Disjointness, and the Universal Class (i); $\mathcal{F}_{Y}$ is a $\sigma$-algebra on $Y$ by Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (xi), so that $(Y,\mathcal{F}_{Y})$ is a measurable space. Let $\mu|_{\mathcal{F}_{Y}}$ be the restriction of $\mu$ to $\mathcal{F}_{Y}$, so $\mu|_{\mathcal{F}_{Y}}$ is a map $\mathcal{F}_{Y}\to[0,\infty]$ with $\mu|_{\mathcal{F}_{Y}}(A)=\mu(A)$ for $A\in\mathcal{F}_{Y}$ (Domains and Restrictions of Maps (ii) and Domains and Restrictions of Maps (iii), as $\mathcal{F}_{Y}\subseteq\mathcal{F}$).

(i) $\mu|_{\mathcal{F}_{Y}}$ is a measure on $(Y,\mathcal{F}_{Y})$.

(ii) If $\mu(Y)<\infty$, then $\mu|_{\mathcal{F}_{Y}}$ is finite.

(iii) There is exactly one map $\nu:\mathcal{F}\to[0,\infty]$ with $\nu(A)=\mu(A\cap Y)$ for every $A\in\mathcal{F}$, where $A\cap Y\in\mathcal{F}$ by Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (ix). This map $\nu$ is a measure on $(X,\mathcal{F})$.

(iv) The map $\nu$ of (iii) satisfies $\nu(X)=\mu(Y)$.

(v) If $\mu$ is $\sigma$-finite, then $\mu|_{\mathcal{F}_{Y}}$ and the map $\nu$ of (iii) are $\sigma$-finite.