avewright/proofwiki-math huggingface dataset:
Theorem: Set Products on Same Set are Equivalent

Let $S$ and $T$ be sets.
Let $\struct {P, \phi_1, \phi_2}$ and $\struct {Q, \psi_1, \psi_2}$ be products of $S$ and $T$.
Then there exists a unique bijection $\chi: Q \to P$ such that:
:$\phi_1 \circ \chi = \psi_1$
:$\phi_2 \circ \chi = \psi_2$

Proof:
We have that $\struct {P, \phi_1, \phi_2}$ is a set product.
From the definition of set product $\chi: Q \to P$ is the unique mapping such that:
:$\phi_1 \circ \chi = \psi_1$
:$\phi_2 \circ \chi = \psi_2$
Similarly, we have that $\struct {Q, \psi_1, \psi_2}$ is a set product.
So from the definition of set product there exists a unique mapping $\xi: P \to Q$ such that:
:$\psi_1 \circ \xi = \phi_1$
:$\psi_2 \circ \xi = \phi_2$
It can be seen that $\chi \circ \xi: P \to P$ is the unique mapping such that:
:$\phi_1 \circ \chi \circ \xi = \phi_1$
:$\phi_2 \circ \chi \circ \xi = \phi_2$
and similarly that $\xi \circ \chi: Q \to Q$ is the unique mapping such that:
:$\psi_1 \circ \xi \circ \chi = \psi_1$
:$\psi_2 \circ \xi \circ \chi = \psi_2$
So it appears that:
:$\chi \circ \xi = I_P$
:$\xi \circ \chi = I_Q$
where $I_P$ and $I_Q$ are the identity mappings on $P$ and $Q$ respectively.
From the corollary to Bijection iff Left and Right Inverse it follows that $\chi$ and $\xi$ are bijections such that $\chi = \xi^{-1}$.
{{qed}}
Theorem: Positive Rational Number as Power of Number with Power of Itself

Every positive rational number can be written either as:
: $a^{a^a}$ for some irrational number $a$
or as:
: $n^{n^n}$ for some natural number $n$.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d x} } {x^{x^x} }
      | r = \map {\frac \d {\d x} } {e^{x^x \ln x} }
}}
{{eqn | r = e^{x^x \ln x} \map {\frac \d {\d x} } {x^x \ln x}
      | c = Chain Rule for Derivatives
}}
{{eqn | r = x^{x^x} \paren {x^x \map {\frac \d {\d x} } {\ln x} + \map {\frac \d {\d x} } {x^x} \ln x}
      | c = Product Rule for Derivatives
}}
{{eqn | r = x^{x^x} \paren {x^x \frac 1 x + x^x \ln x \paren {\ln x + 1} }
      | c = Derivative of Natural Logarithm Function, Derivative of $x^x$
}}
{{eqn | r = x^{x^x + x} \paren {\frac 1 x + \ln x \paren {\ln x + 1} }
}}
{{end-eqn}}
For $\ln x \le 0$ and $\ln x \ge -1$, the above is positive.
For $-1 < \ln x < 0$, we have $e^{-1} < x < 1$.
{{begin-eqn}}
{{eqn | l = x^{x^x + x} \paren {\frac 1 x + \ln x \paren {\ln x + 1} }
      | o = >
      | r = x^{x^x + x} \paren {\frac 1 1 + \paren {-1} \paren {0 + 1} }
}}
{{eqn | r = 0}}
{{end-eqn}}
so we have $\dfrac \d {\d x} x^{x^x} > 0$ for every $x > 0$.
We also have:
:$\ds \lim_{x \mathop \to 0^+} x^{x^x} = \lim_{x \mathop \to 0^+} x^{\lim_{x \mathop \to 0^+} x^x} = 0^1 = 0$
Thus $x^{x^x}: \R_{>0} \to \R_{>0}$ is bijective.
For each $y > 0$, we can find some $x > 0$ such that $y = x^{x^x}$.
The result above is therefore equivalent to:
:$a^{a^a}$ is irrational if $a$ is rational and not a natural number.
By Rational Number as Power of Number with Itself, as long as $a$ is not a natural number, $a^a$ is irrational.
Therefore if $a$ is not a natural number, by Gelfond-Schneider Theorem, $a^{a^a}$ is transcendental, so it is also irrational.
This proves the result.
{{qed}}
Theorem: Rational Number as Power of Number with Itself

Every rational number in the interval $\openint {\paren {\dfrac 1 e}^{\frac 1 e} }{+\infty}$ can be written either as:
: $a^a$ for some irrational number $a$
or as:
: $n^n$ for some natural number $n$.

Proof:
$\dfrac \d {\d x} x^x = \dfrac \d {\d x} e^{x \ln x} = e^{x \ln x} \paren {\ln x + 1}$
So we have $\dfrac \d {\d x} x^x > 0$ for every $x > \dfrac 1 e$.
Thus $x^x: \openint {\dfrac 1 e} {+\infty} \to \openint {\paren {\dfrac 1 e}^{\frac 1 e} } {+\infty}$ is bijective.
For each $y \in \openint {\paren {\dfrac 1 e}^{\frac 1 e} } {+\infty}$, we can find some $x \in \openint {\dfrac 1 e} {+\infty}$ such that $y = x^x$.
The result above is therefore equivalent to:
:$a^a$ is irrational if $a$ is rational and not a natural number.
Suppose $a^a$ is rational for some rational number $a > \dfrac 1 e$.
We express $a^a$ and $a$ in canonical form: 
:$\paren {\dfrac m n}^{\frac m n} = \dfrac b c$
where $m, n, b, c \in \N_{> 0}$ and $\map \gcd {b, c} = \map \gcd {m, n} = 1$.
This gives $\dfrac {m^m} {n^m} = \dfrac {b^n} {c^n}$.
By Canonical Form of Rational Number is Unique:
:$n^m = c^n$
If $n = 1$ then $a = \dfrac m n$ is a natural number, and $a^a$ is rational.
{{AimForCont}} $n \ge 1$.
Then there is a prime such that $p \divides n$.
This prime must also divide $c$.
Write $n = p^i k$, $c = p^j l$, where $i, j, k, l \in \N_{> 0}$ and $\map \gcd {p, k} = \map \gcd {p, l} = 1$.
Then $n^m = p^{i m} k^m = p^{j n} l^n = c^n$.
Since $\map \gcd {p, k^m} = \map \gcd {p, l^n} = 1$, we must have $p^{i m} = p^{j n}$.
Thus $i m = j n = j k p^i$.
Since $\map \gcd {m, n} = 1$, $p \nmid m$.
So we have $p^i \divides i$.
By Absolute Value of Integer is not less than Divisors, $p^i \le i$.
However by Bernoulli's Inequality:
:$p^i \ge 2^i \ge 1 + i > i$
This is a contradiction.
Therefore if $a$ is not a natural number, $a^a$ is irrational.
This proves the result.
{{qed}}
Theorem: Pointwise Sum of Integrable Functions is Integrable Function

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f, g: X \to \overline \R$ be $\mu$-integrable functions.
Suppose that their pointwise sum $f + g$ is well-defined.
Then $f + g$ is also a $\mu$-integrable function.
That is, the space of $\mu$-integrable functions $\LL^1_{\overline \R}$ is closed under pointwise addition.

Proof:
We are given $f, g: X \to \overline \R$ are $\mu$-integrable functions:
{{begin-eqn}}
{{eqn | l = \int f^+ \rd \mu
      | o = <
      | r = +\infty
}}
{{eqn | l = \int f^- \rd \mu
      | o = <
      | r = +\infty
}}
{{end-eqn}}
where $f^+$ and $f^-$ are the positive and negative parts of $f$ respectively.
Also:
{{begin-eqn}}
{{eqn | l = \int g^+ \rd \mu
      | o = <
      | r = +\infty
}}
{{eqn | l = \int g^- \rd \mu
      | o = <
      | r = +\infty
}}
{{end-eqn}}
We are given that pointwise sum $f + g$ is well-defined.
So by Bound for Positive Part of Pointwise Sum of Functions, there exists no $x \in X$ such that:
:$\set {\map f x, \map g x} = \set {\infty, -\infty}$
and:
:$\paren {f + g}^+ \le f^+ + g^+$
By Bound for Negative Part of Pointwise Sum of Functions, there exists no $x \in X$ such that:
:$\set {\map f x, \map g x} = \set {\infty, -\infty}$ 
and:
:$\paren {f + g}^- \le f^- + g^-$
{{finish|Link to below conclusion should be included}}
Therefore:
{{begin-eqn}}
{{eqn | l = \int \paren {f + g}^+ \rd \mu
      | o = <
      | r = +\infty
}}
{{eqn | l = \int \paren {f + g}^- \rd \mu
      | o = <
      | r = +\infty
}}
{{end-eqn}}
Hence $f + g$ is also a $\mu$-integrable function.
{{qed}}
Theorem: Integral of Integrable Function is Monotone

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f, g: X \to \overline \R$ be $\mu$-integrable functions.
Suppose that $f \le g$ pointwise.
Then:
:$\ds \int f \rd \mu \le \int g \rd \mu$

Proof:
Since: 
:$f \le g$
we have that $g - f$ is well-defined with: 
:$g - f \ge 0$
From {{Corollary|Integral of Integrable Function is Additive|2}}, we have: 
:$g - f$ is $\mu$-integrable
with:
:$\ds \int \paren {g - f} \rd \mu = \int g \rd \mu - \int f \rd \mu$
Since: 
:$\ds \int \paren {g - f} \rd \mu \ge 0$
we have:
:$\ds \int g \rd \mu - \int f \rd \mu \ge 0$
This gives:
:$\ds \int g \rd \mu \ge \int f \rd \mu$
{{qed}}
Theorem: Triangle Inequality for Integrals

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f: X \to \overline \R$ be a $\mu$-integrable function.
Then:
:$\ds \size {\int_X f \rd \mu} \le \int_X \size f \rd \mu$

Proof:
We have: 
{{begin-eqn}}
{{eqn | l = \size {\int f \rd \mu}
      | r = \size {\int f^+ \rd \mu - \int f^- \rd \mu}
      | c = {{Defof|Integral of Measure-Integrable Function}}
}}
{{eqn | o = \le
      | r = \size {\int f^+ \rd \mu} + \size {-\int f^- \rd \mu}
      | c = Triangle Inequality for Real Numbers, since $f$ is $\mu$-integrable both integrals are certainly real
}}
{{eqn | r = \int f^+ \rd \mu + \int f^- \rd \mu
}}
{{eqn | r = \int \paren {f^+ + f^-} \rd \mu
      | c = Integral of Positive Measurable Function is Additive
}}
{{eqn | r = \int \size f \rd \mu
      | c = Sum of Positive and Negative Parts
}}
{{end-eqn}}
{{qed}}
Theorem: Measure with Density is Measure

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f: X \to \overline \R_{\ge 0}$ be a positive $\Sigma$-measurable function.
Then the $f \mu$, the measure with density $f$ with respect to $\mu$ is a measure.

Proof:
Note that for each $A \in \Sigma$, we have: 
:$\ds \map {\paren {f \mu} } A = \int_A f \rd \mu$ 
We verify each of the three conditions for a measure.
Theorem: Measurable Function Zero A.E. iff Absolute Value has Zero Integral

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f: X \to \overline \R$ be a $\Sigma$-measurable function.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$f {{=}} 0$ almost everywhere}}
{{item|(2):|$\ds \int \size f \rd \mu {{=}} 0$}}
{{end-itemize}}

Proof:
Let $\EE^+$ be the space of positive simple functions.
Theorem: Integral of Integrable Function over Null Set

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f: X \to \overline \R$ be a $\mu$-integrable function.
Let $N$ be a $\mu$-null set.
Then:
:$\ds \int_N f \rd \mu = 0$
where $\ds \int_N$ signifies an integral over $N$.

Proof:
We have, by definition: 
:$\ds \int_N f \rd \mu = \int f \cdot \chi_N \rd \mu$ 
Note that if $x \in X \setminus N$, we have: 
:$\map {\chi_N} x = 0$
So, if: 
:$\map f x \map {\chi_N} x \ne 0$
we must have $x \in N$. 
Since $N$ is a null set, this gives:
:$f \cdot \chi_N = 0$ $\mu$-almost everywhere. 
From Measurable Function Zero A.E. iff Absolute Value has Zero Integral, we therefore have: 
:$\ds \int \size {f \cdot \chi_N} \rd \mu = 0$ 
Then, from {{Corollary|Triangle Inequality for Integrals}}, we have:
:$\ds \int f \cdot \chi_N \rd \mu = 0$
That is: 
:$\ds \int_N f \rd \mu = 0$
{{qed}}
Theorem: A.E. Equal Positive Measurable Functions have Equal Integrals

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f, g: X \to \overline \R_{\ge 0}$ be positive $\Sigma$-measurable functions.
Suppose that $f = g$ almost everywhere.
Then:
:$\ds \int f \rd \mu = \int g \rd \mu$

Proof:
Let: 
:$A = \set {x \in X : \map f x \ne \map g x}$
From Measurable Functions Determine Measurable Sets, we have that: 
:$A$ is $\Sigma$-measurable.
Define $h : X \to \overline \R$ by: 
:$\map h x = \begin{cases}+\infty & x \in A \\ 0 & x \not \in A\end{cases}$
We can show that $h$ is $\Sigma$-measurable.
If $t < 0$, we have that: 
:$\set {x \in X : \map h x \le t} = \O$
From Sigma-Algebra Contains Empty Set, we therefore have that: 
:$\set {x \in X : \map h x \le t}$ is $\Sigma$-measurable if $t < 0$. 
If $t \ge 0$, we have that: 
:$\set {x \in X : \map h x \le t} = X \setminus A$
This is also $\Sigma$-measurable, so $h$ is a $\Sigma$-measurable function.
Clearly also $h \ge 0$. 
We can show that: 
:$f \le g + h$ 
If $x \in A$, then $\map h x = +\infty$, so $\map g x + \map h x = +\infty$, and the inequality is satisfied trivially.
If $x \not \in A$, we have $\map f x = \map g x = \map g x + \map h x$, and so $\map f x \le \map g x + \map h x$ again.
From Integral of Positive Measurable Function is Monotone, we then have: 
:$\ds \int f \rd \mu \le \int \paren {g + h} \rd \mu$
Applying Integral of Integrable Function is Additive, we then have: 
:$\ds \int f \rd \mu \le \int g \rd \mu + \int h \rd \mu$
To compute the latter integral, note that: 
:$x \in X$ is such that $\map h x \ne 0$ {{iff}} $x \in A$.
Since by hypothesis, $f = g$ $\mu$-almost everywhere, we have that: 
:$\map \mu A = 0$ 
So:
:$h = 0$ $\mu$-almost everywhere.
Then, by Measurable Function Zero A.E. iff Absolute Value has Zero Integral, we have: 
:$\ds \int \size h \rd \mu = 0$
Since $h \ge 0$, this gives: 
:$\ds \int h \rd \mu = 0$
and so: 
:$\ds \int f \rd \mu \le \int g \rd \mu$
Similarly, we have: 
:$g \le f + h$
and obtain: 
:$\ds \int g \rd \mu \le \int f \rd \mu$
simply swapping $g$ for $f$ in the prior computation. 
We therefore have: 
:$\ds \int f \rd \mu = \int g \rd \mu$
{{qed}}
Theorem: Integrable Function is A.E. Real-Valued

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f: X \to \overline \R$ be a $\mu$-integrable function.
Then $\map f x \in \R$ for almost all $x \in X$.

Proof:
From {{Corollary|Set of Points for which Measurable Function is Real-Valued is Measurable}}, we have that: 
:$\set {x \in X : \size {\map f x} = +\infty}$ is $\Sigma$-measurable.
We now aim to show that this set is a null set. 
Now note that we have:
:$\set {x \in X : \size {\map f x} = +\infty} \subseteq \set {x \in X : \size {\map f x} \ge n}$
From Measure is Monotone, we therefore have: 
:$\ds \map \mu {\set {x \in X : \size {\map f x} = +\infty} } \le \map \mu {\set {x \in X : \size {\map f x} \ge n} }$
From Markov's Inequality, we have: 
:$\ds \map \mu {\set {x \in X : \size {\map f x} \ge n} } \le \frac 1 n \int \size f \rd \mu$
So:
:$\ds 0 \le \map \mu {\set {x \in X : \size {\map f x} = +\infty} } \le \frac 1 n \int \size f \rd \mu$
for each $n \in \N$.
From Lower and Upper Bounds for Sequences, taking $n \to \infty$, we obtain:
:$\ds \map \mu {\set {x \in X : \size {\map f x} = +\infty} } = 0$ 
That is: 
:$\ds \map \mu {X \setminus \set {x \in X : \map f x \in \R} } = 0$
So: 
:$\map f x \in \R$ for almost all $x \in X$.
{{qed}}
Theorem: Measurable Functions with Equal Integrals on Sub-Sigma-Algebra are A.E. Equal

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $\GG$ be a sub-$\sigma$-algebra of $\Sigma$.
Suppose that $\mu \restriction_\GG$, the restriction of $\mu$ to $\GG$, is $\sigma$-finite.
Let $f, g: X \to \overline \R$ be $\GG$-measurable functions.
Suppose that, for all $G \in \GG$:
:$\ds \int_G f \rd \mu = \int_G g \rd \mu$
Then $f = g$ $\mu$-almost everywhere.

Proof:
First, assume that $f$ and $g$ are $\mu$-integrable.
Observe:
{{begin-eqn}}
{{eqn | n = 1
      | l = \set {f \ne g}
      | r = \bigcup_{n \mathop = 1}^\infty \set {\size {f - g} \ge \dfrac 1 n }
}}
{{end-eqn}}
For each $n \in \N_{>0}$:
{{begin-eqn}}
{{eqn | l = \map \mu {\set {f - g \ge \dfrac 1 n} }
      | r = \int_{\set {f - g \ge \frac{1}{n} } } 1 \rd \mu
}}
{{eqn | r = n \int_{\set {f - g \ge \frac{1}{n} } } \dfrac 1 n \rd \mu
}}
{{eqn | o = \le
      | r = n \int_{\set {f - g \ge \frac{1}{n} } } \paren {f - g} \rd \mu
}}
{{eqn | r = n \paren {\int_{\set {f - g \ge \frac{1}{n} } } f \rd \mu - \int_{\set {f - g \ge \frac{1}{n} } } g \rd \mu}
}}
{{eqn | r = 0
      | c = {{hypothesis}} as $\set {f - g \ge \dfrac 1 n} \in \GG$
}}
{{end-eqn}}
Swapping $f$ and $g$, we also have:
{{begin-eqn}}
{{eqn | l = \map \mu {\set {g - f \ge \dfrac 1 n} }
      | r = 0
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | n = 2
      | l = \map \mu {\set {\size {f - g} \ge \dfrac 1 n} }
      | r = \map \mu {\set {f - g \ge \dfrac 1 n} } + \map \mu {\set {g - f \ge \dfrac 1 n} }
}}
{{eqn | r = 0
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = \map \mu {\set {f \ne g} }
      | r = \map \mu {\bigcup_{n \mathop = 1}^\infty \set {\size {f - g} \ge \dfrac 1 n } }
      | c = by $\paren 1$
}}
{{eqn | o = \le
      | r = \sum _{n \mathop = 1}^\infty \map \mu { \set {\size {f - g} \ge \dfrac 1 n } }
}}
{{eqn | r = 0
      | c = by $\paren 2$
}}
{{end-eqn}}
Hence the result, by definition of almost-everywhere equality.
{{qed|lemma}}
Now, consider general $f$ and $g$.
Recall that $\mu \restriction_\GG$　is $\sigma$-finite.
That is, there is an exhausting sequence $\sequence {E_n}_{n\in\N} \subseteq \GG$ such that:
:$\map \mu {E_n} < \infty$
We define $\sequence {A_n}_{n\in\N} \subseteq \GG$ by:
:$A_n := E_n \cap \set { \size f \le n} \cap \set {\size g \le n}$
Then $\sequence {A_n}_{n\in\N}$ is also an exhausting sequence.
Let $f_n := f \chi_{A_n}$ and $g_n := g \chi_{A_n}$.
Then $f_n$ and $g_n$ are $\mu$-integrable so that:
:$\forall n \in \N : \map \mu {\set {f_n \ne g_n} } = 0$
On the other hand:
:$\set {f_n \ne g_n} = \set {f \ne g} \cap A_n$
Therefore:
{{begin-eqn}}
{{eqn | l = \map \mu {\set {f \ne g} }
      | r = \lim_{n \mathop \to \infty} \map \mu {\set {f \ne g} \cap A_n }
      | c = Measure of Limit of Increasing Sequence of Measurable Sets
}}
{{eqn | r = \lim_{n \mathop \to \infty} \map \mu {\set {f_n \ne g_n} }
}}
{{eqn | r = 0
}}
{{end-eqn}}
{{qed}}
Theorem: Intersection is Largest Subset/Family of Sets

Let $\family {S_i}_{i \mathop \in I}$ be a family of sets indexed by $I$.
Then for all sets $X$:
:$\ds \paren {\forall i \in I: X \subseteq S_i} \iff X \subseteq \bigcap_{i \mathop \in I} S_i$
where $\ds \bigcap_{i \mathop \in I} S_i$ is the intersection of $\family {S_i}$.

Proof:
Let $X \subseteq S_i$ for all $i \in I$.
Then from Set is Subset of Intersection of Supersets: General Result:
:$\ds X \subseteq \bigcap_{i \mathop \in I} S_i$
{{qed|lemma}}
Now suppose that $\ds X \subseteq \bigcap_{i \mathop \in I} S_i$.
From Intersection is Subset: Family of Sets we have:
:$\ds \forall i \in I: \bigcap_{j \mathop \in I} S_j \subseteq S_i$
So from Subset Relation is Transitive, it follows that:
:$\ds \forall i \in I: X \subseteq \bigcap_{j \mathop \in I} S_j \subseteq S_i$
So it follows that $\forall i \in I: X \subseteq S_i$.
So:
:$\ds X \subseteq \bigcap_{i \mathop \in I} S_i \implies \paren {\forall i \in I: X \subseteq S_i}$
{{qed|lemma}}
Hence:
:$\ds \paren {\forall i \in I: X \subseteq S_i} \iff X \subseteq \bigcap_{i \mathop \in I} S_i$
{{Qed}}
Theorem: Countable Set is Null Set under Lebesgue Measure

Let $S \subseteq \R$ be a countable set.
Then $\map \lambda S = 0$, where $\lambda$ is Lebesgue measure.
That is, $S$ is a $\lambda$-null set.

Proof:
By Surjection from Natural Numbers iff Countable, there exists a surjection $f: \N \to S$.
It follows that:
:$S = \ds \bigcup_{n \mathop \in \N} \set{\map f n}$
As Lebesgue Measure is Diffuse, it holds that:
:$\forall n \in \N: \map \lambda {\set{\map f n}} = 0$
Thus, by Null Sets Closed under Countable Union, it follows that:
:$\map \lambda S = 0$
{{qed}}
Theorem: Intersection is Subset/Family of Sets

Let $\family {S_\alpha}_{\alpha \mathop \in I}$ be a family of sets indexed by $I$.
Then:
:$\ds \forall \beta \in I: \bigcap_{\alpha \mathop \in I} S_\alpha \subseteq S_\beta$
where $\ds \bigcap_{\alpha \mathop \in I} S_\alpha$ is the intersection of $\family {S_\alpha}_{\alpha \mathop \in I}$.

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \bigcap_{\alpha \mathop \in I} S_\alpha
      | c =
}}
{{eqn | ll= \leadsto
      | q = \forall \beta \in I
      | l = x
      | o = \in
      | r = S_\beta
      | c = {{Defof|Intersection of Family}}
}}
{{eqn | ll= \leadsto
      | q = \forall \beta \in I
      | l = \bigcap_{\alpha \mathop \in I} S_\alpha
      | o = \subseteq
      | r = S_\beta
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{qed}}
Theorem: Union is Smallest Superset/Family of Sets

Let $\family {S_i}_{i \mathop \in I}$ be a family of sets indexed by $I$.
Then for all sets $X$:
:$\ds \paren {\forall i \in I: S_i \subseteq X} \iff \bigcup_{i \mathop \in I} S_i \subseteq X$
where $\ds \bigcup_{i \mathop \in I} S_i$ is the union of $\family {S_i}$.

Proof:
=== Necessary Condition ===
From Union of Family of Subsets is Subset we have that:
:$\ds \paren {\forall i \in I: S_i \subseteq X} \implies \bigcup_{i \mathop \in I} S_i \subseteq X$
{{qed|lemma}}
Theorem: Fatou's Lemma for Integrals/Integrable Functions

Let $\sequence {f_n}_{n \mathop \in \N} \in \LL^1$, $f_n: X \to \R$ be a sequence of $\mu$-integrable functions.
Let $\ds \liminf_{n \mathop \to \infty} f_n: X \to \overline \R$ be the pointwise limit inferior of the $f_n$.
Suppose that there exists an $\mu$-integrable $f: X \to \R$ such that for all $n \in \N$, $f \le f_n$ pointwise.
Then:
:$\ds \int \liminf_{n \mathop \to \infty} f_n \rd \mu \le \liminf_{n \mathop \to \infty} \int f_n \rd \mu$
where:
:the integral sign denotes $\mu$-integration
:the {{RHS}} limit inferior is taken in the extended real numbers $\overline \R$.

Proof:
{{ProofWanted}}
{{Namedfor|Pierre Joseph Louis Fatou|cat = Fatou}}
Theorem: Fatou's Lemma for Integrals/Positive Measurable Functions

Let $\sequence {f_n}_{n \mathop \in \N} \in \MM_{\overline \R}^+$, $f_n: X \to \overline \R$ be a sequence of positive measurable functions.
{{explain|What is $\MM_{\overline \R}^+$?}}
Let $\ds \liminf_{n \mathop \to \infty} f_n: X \to \overline \R$ be the pointwise limit inferior of the $f_n$.
Then:
:$\ds \int \liminf_{n \mathop \to \infty} f_n \rd \mu \le \liminf_{n \mathop \to \infty} \int f_n \rd \mu$
where:
:the integral sign denotes $\mu$-integration
:the {{RHS}} limit inferior is taken in the extended real numbers $\overline \R$.

Proof:
For each $n \in \N$, define $g_n : X \to \overline \R$ by: 
:$\ds g_n = \inf_{k \mathop \ge n} f_k$
That is: 
:$\map {g_n} x = \inf \set {\map {f_k} x : k \ge n}$
for each $x \in X$. 
For each $n \in \N$, we have that: 
:$\set {\map {f_k} x : k \ge n + 1} \subseteq \set {\map {f_k} x : k \ge n}$
From Infimum of Subset: 
:$\inf \set {\map {f_k} x : k \ge n + 1} \ge \inf \set {\map {f_k} x : k \ge n}$
That is: 
:$\map {g_{n + 1} } x \ge \map {g_n} x$
for each $n \in \N$. 
From Pointwise Infimum of Measurable Functions is Measurable, we also have: 
:$g_n$ is $\Sigma$-measurable for each $n \in \N$. 
We have: 
:$\ds \lim_{n \mathop \to \infty} g_n = \lim_{n \mathop \to \infty} \paren {\inf_{k \mathop \ge n} f_k}$
By the definition of limit inferior: 
:$\ds \lim_{n \mathop \to \infty} g_n = \liminf_{n \mathop \to \infty} f_n$
So:
:$\sequence {g_n}_{n \mathop \in \N}$ is an increasing sequence of $\Sigma$-measurable functions convergent to $\ds \liminf_{n \mathop \to \infty} f_n$.
We are therefore able to apply the monotone convergence theorem.
We then have:: 
{{begin-eqn}}
{{eqn	| l = \int \liminf_{n \mathop \to \infty} f_n \rd \mu
	| r = \int \lim_{n \mathop \to \infty} \paren {\inf_{k \mathop \ge n} f_k} \rd \mu
}}
{{eqn	| r = \lim_{n \mathop \to \infty} \int \paren {\inf_{k \mathop \ge n} f_k} \rd \mu
	| c = applying the monotone convergence theorem to $\sequence {g_n}_{n \mathop \in \N}$
}}
{{end-eqn}}
Clearly we have: 
:$\ds \inf_{k \mathop \ge n} f_k \le f_n$
for any $n \in \N$. 
So, by Integral of Integrable Function is Monotone: 
:$\ds \int \paren {\inf_{k \mathop \ge n} f_k} \rd \mu \le \int f_n \rd \mu$ 
and so: 
:$\ds \int \paren {\inf_{k \mathop \ge n} f_k} \rd \mu \le \inf_{k \mathop \ge n} \int f_k \rd \mu$ 
Then: 
{{begin-eqn}}
{{eqn	| l = \lim_{n \mathop \to \infty} \int \paren {\inf_{k \mathop \ge n} f_k} \rd \mu
	| o = \le
	| r = \lim_{n \mathop \to \infty} \paren {\inf_{k \mathop \ge n} \int f_k \rd \mu}
}}
{{eqn	| r = \liminf_{n \mathop \to \infty} \int f_n \rd \mu
}}
{{end-eqn}}
{{qed}}
Theorem: Reverse Fatou's Lemma/Integrable Functions

Let $\sequence {f_n}_{n \mathop \in \N} \in \LL^1$, $f_n: X \to \R$ be a sequence of $\mu$-integrable functions.
{{mistake|$f_n \in \LL^1$ for each $n$}}
Let $\ds \limsup_{n \mathop \to \infty} f_n: X \to \overline \R$ be the pointwise limit superior of the $f_n$.
Suppose that there exists an $\mu$-integrable $f: X \to \R$ such that for all $n \in \N$, $f_n \le f$ pointwise.
Then:
:$\ds \limsup_{n \mathop \to \infty} \int f_n \rd \mu \le \int \limsup_{n \mathop \to \infty} f_n \rd \mu$
where:
:the integral sign denotes $\mu$-integration
:the {{RHS}} limit inferior is taken in the extended real numbers $\overline \R$.

Proof:
{{ProofWanted}}
{{Namedfor|Pierre Joseph Louis Fatou|cat = Fatou}}