Proof of Fatou's Lemma

Throughout, $\le$ on $[-\infty,\infty]$ is a total order (Order and Suprema in the Extended Real Line (i)), and every subset of $[-\infty,\infty]$ has a supremum and an infimum (Order and Suprema in the Extended Real Line (iii)). By Nonnegative Measurable Maps and Their Lebesgue Integral (i), $(f_{m})$ is a sequence in $\mathrm{Meas}(X,\mathcal{F};[0,\infty],\mathcal{B}([0,\infty]))$, so Suprema, Infima, Limits Inferior and Limits Superior of Measurable [0,∞]-Valued Maps applies to it. Each $f_{m}$ is a map $X\to[0,\infty]$, so an element of $[0,\infty]^{X}$ and, as $[0,\infty]\subseteq[-\infty,\infty]$ (The Extended Real Line, Its Order, and [0,∞] (ii)), of $[-\infty,\infty]^{X}$ (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)); thus $(f_{m})$ is a sequence in $[0,\infty]^{X}$ and in $[-\infty,\infty]^{X}$, as Maps Used to Build the Integral: Fibres of a Map, Pointwise Combinations with Finite Image, Tail Extrema of a Sequence of Maps, the Integer Part, and Indicators (iii) requires. For $x\in X$ let $a^{x}$ be the sequence in $[0,\infty]$ with $a^{x}_{m}=f_{m}(x)$ for every $m\in\mathbb{N}$ (Evaluating a Sequence of Maps at a Point Gives a Sequence, and Its Range (i)); so $\liminf_{m}f_{m}(x)$ is $\liminf_{m}a^{x}_{m}$, and $g(x)=\liminf_{m}a^{x}_{m}$.

Proof of (i). By Suprema, Infima, Limits Inferior and Limits Superior of Measurable [0,∞]-Valued Maps (iii), the map $x\mapsto\sup_{k}\inf\{f_{m}(x):m\in\mathbb{N},\ m\ge k\}$ from $X$ to $[0,\infty]$ is measurable. It is $g$, as both have the value $\liminf_{m}a^{x}_{m}=\sup_{k}\inf\{a^{x}_{m}:m\in\mathbb{N},\ m\ge k\}$ at every $x\in X$, with $a^{x}_{m}=f_{m}(x)$ (Tail Extrema, Limit Inferior and Limit Superior of a Sequence in [−∞,∞] (ii), Tail Extrema, Limit Inferior and Limit Superior of a Sequence in [−∞,∞] (i)), and maps with equal values are equal (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv)). So $g\in\mathcal{M}^{+}$ by Nonnegative Measurable Maps and Their Lebesgue Integral (i).

Proof of (ii). By Maps Used to Build the Integral: Fibres of a Map, Pointwise Combinations with Finite Image, Tail Extrema of a Sequence of Maps, the Integer Part, and Indicators (iii), there is a sequence $(g_{k})$ of maps $X\to[-\infty,\infty]$ with $g_{k}(x)=\inf_{m\ge k}f_{m}(x)=\inf\{f_{m}(x):m\in\mathbb{N},\ m\ge k\}$ for all $k\in\mathbb{N}$ and $x\in X$. By Suprema, Infima, Limits Inferior and Limits Superior of Measurable [0,∞]-Valued Maps (ii), applied to $J=\{m\in\mathbb{N}:m\ge k\}$, each $g_{k}$ takes values in $[0,\infty]$ and is measurable, so $(g_{k})$ is a sequence in $\mathcal{M}^{+}$ (Nonnegative Measurable Maps and Their Lebesgue Integral (i)).

$(g_{k})$ is nondecreasing. Let $k\in\mathbb{N}$. If $m\in\mathbb{N}$ and $m\ge k+1$, then $m\ge k$: $k<k+1$ by Arithmetic and Order of the Natural Numbers (xi), so $k\le k+1$ and $k\le m$ by Arithmetic and Order of the Natural Numbers (vi). So for $x\in X$, $\{f_{m}(x):m\in\mathbb{N},\ m\ge k+1\}\subseteq\{f_{m}(x):m\in\mathbb{N},\ m\ge k\}$, and $g_{k}(x)\le g_{k+1}(x)$ by Greatest Elements as Suprema, Suprema and Infima of Nested Sets in [−∞,∞], and a Scaling Criterion for Order in [0,∞] (ii).

Monotone convergence. Let $x\in X$. Let $u$ be the sequence in $[-\infty,\infty]$ with $u_{k}=g_{k}(x)$ for every $k\in\mathbb{N}$ (Evaluating a Sequence of Maps at a Point Gives a Sequence, and Its Range (i)), $(g_{k})$ being a sequence in $[-\infty,\infty]^{X}$. Its range is $\{g_{k}(x):k\in\mathbb{N}\}$ (Evaluating a Sequence of Maps at a Point Gives a Sequence, and Its Range (ii)), that is $\{\inf_{m\ge k}a^{x}_{m}:k\in\mathbb{N}\}$ (Maps Used to Build the Integral: Fibres of a Map, Pointwise Combinations with Finite Image, Tail Extrema of a Sequence of Maps, the Integer Part, and Indicators (iii), Tail Extrema, Limit Inferior and Limit Superior of a Sequence in [−∞,∞] (i)); so $g(x)=\liminf_{m}a^{x}_{m}$ is the supremum of the range of $u$ (Tail Extrema, Limit Inferior and Limit Superior of a Sequence in [−∞,∞] (ii)), that is $g(x)=\sup_{k}g_{k}(x)$. The sequence $k\mapsto\int_{X}g_{k}\,d\mu$ is the composite of $(g_{k})$, a map $\mathbb{N}\to\mathcal{M}^{+}$, with the integral map $\mathcal{M}^{+}\to[0,\infty]$ (Nonnegative Measurable Maps and Their Lebesgue Integral (ii), Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii)), and likewise $m\mapsto\int_{X}f_{m}\,d\mu$ is the composite of $(f_{m})$ with it. So Monotone Convergence Theorem (ii) applies to $(g_{k})$ and $g$ and gives

$$\int_{X}g\,d\mu=\sup_{k}\int_{X}g_{k}\,d\mu.$$

Comparison. Let $k\in\mathbb{N}$ and $\beta_{k}=\inf\{\int_{X}f_{m}\,d\mu:m\in\mathbb{N},\ m\ge k\}$, so that $\liminf_{m}\int_{X}f_{m}\,d\mu=\sup_{k}\beta_{k}$ by Tail Extrema, Limit Inferior and Limit Superior of a Sequence in [−∞,∞] (i) and Tail Extrema, Limit Inferior and Limit Superior of a Sequence in [−∞,∞] (ii), the integrals lying in $[0,\infty]$ by Nonnegative Measurable Maps and Their Lebesgue Integral (ii). For every $m\in\mathbb{N}$ with $m\ge k$ and every $x\in X$, $g_{k}(x)\le f_{m}(x)$, as $g_{k}(x)$ is a lower bound of $\{f_{j}(x):j\ge k\}$ (Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv)); hence $\int_{X}g_{k}\,d\mu\le\int_{X}f_{m}\,d\mu$ by Basic Properties of the Integral of Nonnegative Measurable Maps (iii). So $\int_{X}g_{k}\,d\mu$ is a lower bound of $\{\int_{X}f_{m}\,d\mu:m\ge k\}$, and $\int_{X}g_{k}\,d\mu\le\beta_{k}$, $\beta_{k}$ being its greatest lower bound. Since $\beta_{k}\le\sup_{j}\beta_{j}$, the supremum being an upper bound, $\int_{X}g_{k}\,d\mu\le\liminf_{m}\int_{X}f_{m}\,d\mu$ by transitivity (Order and Suprema in the Extended Real Line (i)). Thus $\liminf_{m}\int_{X}f_{m}\,d\mu$ is an upper bound of $\{\int_{X}g_{k}\,d\mu:k\in\mathbb{N}\}$, and

$$\int_{X}g\,d\mu=\sup_{k}\int_{X}g_{k}\,d\mu\le\liminf_{m}\int_{X}f_{m}\,d\mu,$$

as the supremum is the least upper bound (Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order (iv)).