Measure, Measure Space, and Probability Measure

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $(X,\mathcal{F})$ be a measurable space. Then $X\in\mathcal{F}$ by σ-Algebra and Measurable Space (i), and $\emptyset\in\mathcal{F}$ for the empty set $\emptyset$, by Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (vi). Let $\infty$, $[0,\infty]$ and $<$ be as in The Extended Real Line, Its Order, and [0,∞] (i), The Extended Real Line, Its Order, and [0,∞] (ii) and The Extended Real Line, Its Order, and [0,∞] (iii); $1\in[0,\infty]$ by Addition and Multiplication on [0,∞] (ii). For a sequence $(a_{m})$ in $[0,\infty]$, $\sum_{m\in\mathbb{N}}a_{m}$ is its sum. For a sequence $(A_{m})$ in $\mathcal{F}$, $\bigcup_{m\in\mathbb{N}}A_{m}$ is the union of $(A_{m})$ as a family indexed by $\mathbb{N}$, and $\bigcup_{m\in\mathbb{N}}A_{m}\in\mathcal{F}$ by σ-Algebra and Measurable Space (i); the sequence $(A_{m})$ is pairwise disjoint if $A_{m}\cap A_{k}=\emptyset$ for all $m,k\in\mathbb{N}$ with $m\neq k$, where $\cap$ is the intersection.

(i) A measure on $(X,\mathcal{F})$ is a map $\mu:\mathcal{F}\to[0,\infty]$ such that $\mu(\emptyset)=0$ and

$$\mu\Bigl(\bigcup_{m\in\mathbb{N}}A_{m}\Bigr)=\sum_{m\in\mathbb{N}}\mu(A_{m})$$

for every pairwise disjoint sequence $(A_{m})$ in $\mathcal{F}$, the right-hand side being the sum of the sequence $m\mapsto\mu(A_{m})$ in $[0,\infty]$ (countable additivity).

(ii) A measure space is the tuple $(X,\mathcal{F},\mu)=\langle X,\mathcal{F},\mu\rangle$ of a measurable space $(X,\mathcal{F})$ and a measure $\mu$ on $(X,\mathcal{F})$.

Let $\mu$ be a measure on $(X,\mathcal{F})$.

(iii) $\mu$ is finite if $\mu(X)<\infty$.

(iv) $\mu$ is $\sigma$-finite if there is a sequence $(X_{m})$ in $\mathcal{F}$ with $\bigcup_{m\in\mathbb{N}}X_{m}=X$ and $\mu(X_{m})<\infty$ for every $m\in\mathbb{N}$.

(v) $\mu$ is a probability measure if $\mu(X)=1$.