avewright/proofwiki-math huggingface dataset:
Theorem: Characteristics of Eulerian Graph/Necessary Condition

Let $G$ be a finite (undirected) graph.
Let $G$ be Eulerian.
Then $G$ is connected and each vertex of $G$ is even.
Note that the definition of graph here includes:
* Simple graph
* Loop-graph
* Multigraph
* Loop-multigraph
but does not include directed graph.

Proof:
Suppose that $G$ is Eulerian.
Then $G$ contains an Eulerian circuit, that is, a circuit that uses each vertex and passes through each edge exactly once.
Since a circuit must be connected, $G$ is connected.
Beginning at a vertex $v$, follow the Eulerian circuit through $G$.
As the circuit passes through each vertex, it uses two edges: one going to the vertex and another leaving.
Each edge is used exactly once, so each of the vertices must be even.
Since the circuit must also end at $v$, it follows that $v$ is also even.
{{qed}}
Theorem: Characteristics of Eulerian Graph/Sufficient Condition

Let $G$ be a finite (undirected) graph which is connected
Let each vertex of $G$ be even.
Then $G$ is an Eulerian graph.

Proof:
=== Proof 1 ===
{{:Characteristics of Eulerian Graph/Sufficient Condition/Proof 1}}
=== Proof 2 ===
{{:Characteristics of Eulerian Graph/Sufficient Condition/Proof 2}}
Theorem: Characteristics of Eulerian Graph/Sufficient Condition

Let $G$ be a finite (undirected) graph which is connected
Let each vertex of $G$ be even.
Then $G$ is an Eulerian graph.

Proof:
Suppose that an (undirected) graph $G$ is connected and its vertices all have even degree.
If there is more than one vertex in $G$, then each vertex must have degree greater than $0$.
Begin at a vertex $v$.
From Graph with Even Vertices Partitions into Cycles, we know that $v$ will be on at least one cycle.
Since $G$ is connected, there must be an edge $\set {v, v_1}$ for some vertex $v_1 \ne v$.
Since $v_1$ has even degree greater than $0$, there is an edge $\set {v_1, v_2}$ where $v_2 \ne v_1$.
These two edges make a trail from $v$ to $v_2$.
Continue this trail, leaving each vertex on an edge that was not previously used, until returning to $v$.
This is always possible, because $v$ is on a cycle.
Call the circuit formed by this process $C_1$.
If $C_1$ covers all the edges of $G$, then the proof is complete.
Otherwise, remove all the edges that contribute to $C_1$ from $G$, leaving the graph $G_0$.
The remaining vertices are still even, and since $G$ is connected there is some vertex $u$ in both $G_0$ and $C_1$.
Repeat the same process as before, beginning at $u$.
The new circuit, $C_2$, can be added to $C_1$ by starting at $v$, moving along $C_1$ to $u$, travelling around $C_2$ back to $u$ and then along the remainder of $C_1$ back to $v$.
Repeat this process, adding each new circuit found to create a larger circuit.
Since $G$ is finite, this process must end at some point, and the resulting circuit will be an Eulerian circuit.
{{qed}}
Theorem: Characteristics of Eulerian Graph/Sufficient Condition

Let $G$ be a finite (undirected) graph which is connected
Let each vertex of $G$ be even.
Then $G$ is an Eulerian graph.

Proof:
Suppose that an (undirected) graph $G$ is connected and its vertices all have even degree.
From Graph with Even Vertices Partitions into Cycles, we can split $G$ into a number of cycles $\mathbb S = C_1, C_2, \ldots, C_k$.
Start at any vertex $v$ on cycle $C_1$ and traverse its edges until we encounter a vertex of another cycle of $\mathbb S$, $C_2$ say.
The edges of $C_2$ are then traversed, and then the traversal of $C_1$ is resumed when it is returned to.
As $C_1$ is traversed, the journey is interrupted so as to traverse any other cycles of $\mathbb S$ in the same way that $C_2$ is traversed.
Eventually the beginning of $C_1$ is reached, which is vertex $v$.
Thus there exists a circuit which includes $C_1$ and at least one other cycle (unless $C_1$ is the only cycle), as $G$ is connected.
If this circuit contains all the cycles $C_1, C_2, \ldots, C_k$, the required Eulerian circuit has been found.
If not, then the circuit just generated is traversed.
Because $G$ is connected, other cycles in $\mathbb S$ will be encountered.
These, again, are traversed as they are encountered.
This process is continued till all the cycles have been included in the circuit.
At this stage, the required Eulerian circuit has been found.
Hence $G$ is Eulerian.
{{qed}}
Theorem: Characterization of Pre-Measures

Let $X$ be a set, and let $\SS \subseteq \powerset X$ be a collection of subsets of $X$.
Let $\O \in \SS$.
Denote $\overline \R_{\ge 0}$ for the set of positive extended real numbers.
A mapping $\mu: \SS \to \overline \R_{\ge 0}$ is a pre-measure {{iff}}:
{{begin-itemize}}
{{item|(1):|$\map \mu \O {{=}} 0$}}
{{item|(2):|$\mu$ is finitely additive}}
{{item|(3):|For every increasing sequence $\sequence {E_n}_{n \mathop \in \N}$ in $\SS$, if $E_n \uparrow E$ for some $E \in \SS$, then:
:$\ds \map \mu E {{=}} \lim_{n \mathop \to \infty} \map \mu {E_n}$}}
{{end-itemize}}
where $E_n \uparrow E$ denotes limit of increasing sequence of sets.
Alternatively, and equivalently, $(3)$ may be replaced by either of:
{{begin-itemize}}
{{item|(3'):|For every decreasing sequence $\sequence {E_n}_{n \mathop \in \N}$ in $\SS$ for which $\map \mu {E_1}$ is finite, if $E_n \downarrow E$ for some $E \in \SS$, then:
:$\ds \map \mu E {{=}} \lim_{n \mathop \to \infty} \map \mu {E_n}$}}
{{item|(3' '):|For every decreasing sequence $\sequence {E_n}_{n \mathop \in \N}$ in $\SS$ for which $\map \mu {E_1}$ is finite, if $E_n \downarrow \O$, then:
:$\ds \lim_{n \mathop \to \infty} \map \mu {E_n} {{=}} 0$}}
{{end-itemize}}
where $E_n \downarrow E$ denotes limit of decreasing sequence of sets.

Proof:
{{ProofWanted|will be very similar to Characterization of Measures}}
Category:Pre-Measures
64jdmjdy4nopm4tffbkzqu4uysyt9vd
Theorem: Power Set is Magma of Sets

Let $X$ be a set.
Let $\family {\phi_i}: i \in I$ be an indexed family of mappings.
Then $\powerset X$, the power set of $X$, is a magma of sets for $\family {\phi_i}: i \in I$ on $X$.

Proof:
For every $i \in I$, let $J_i$ be an index set, and let:
:$\phi_i: \powerset X^{J_i} \to \powerset X$
be a partial mapping.
For each $i \in I$, for each $\family {S_{j_i} }_{j_i \mathop \in J_i} \in \powerset X^{J_i} \cap \DD_i$, that:
:$\map {\phi_i} {\family {S_{j_i} }_{j_i \mathop \in J_i} } \in \powerset X$
{{explain|What is \cap \DD_i? Please add explanation for the symbol for clarity.}}
follows directly from the fact that $\powerset X$ is the codomain of $\phi_i$,
for every indexed family $\family {S_j}_{j \mathop \in J_i} \in \SS^{J_i}$ in the domain of $\phi_i$.
Hence $\powerset X$ is a magma of sets for $\family {\phi_i}: i \in I$ on $X$.
{{qed}}
Category:Magmas of Sets
blnmwr0jf8lzo5sj1v25vigohhjrk1o
Theorem: Existence and Uniqueness of Magma of Sets Generated by Collection of Subsets

Let $X$ be a set, and let $\Phi := \set {\phi_i: i \in I}$ be a collection of partial mappings with codomain $\powerset X$, the power set of $X$.
Let $\GG \subseteq \powerset X$ be a collection of subsets of $X$.
Then the magma of sets generated by $\GG$ exists and is unique.

Proof:
=== Uniqueness ===
Suppose that both $\SS$ and $\TT$ are magmas of sets for $\Phi$ generated by $\GG$.
Applying condition $(2)$ for these twice, we obtain:
:$\SS \subseteq \TT$
:$\TT \subseteq \SS$
By definition of set equality:
:$\SS = \TT$
{{qed|lemma}}
Theorem: Intersection of Magmas of Sets is Magma of Sets

Let $X$ be a set.
Let $\Phi := \set {\phi_i: i \in I}$ be a collection of partial mappings with codomain $\powerset X$, the power set of $X$.
Let $\SS_j$ be a magma of sets for $\Phi$, for each $j \in J$, for some index set $J$.
Then:
:$\SS := \ds \bigcap_{j \mathop \in J} \SS_j$
is also a magma of sets for $\Phi$.

Proof:
{{explain|the notation in the below}}
For each $i \in I$ and $j \in J$, we have:
:$\map {\phi_i} {\sequence {S_{j, j_i} }_{j_i \mathop \in J_i} } \in \SS_j$
Thus, if for each $j \in J$, one has:
:$(1): \quad \sequence {S_{j_i} }_{j_i \mathop \in J_i} \in \SS_j^{J_i}$
it follows from definition of set intersection that:
:$\map {\phi_i} {\sequence {S_{j_i} }_{j_i \mathop \in J_i} } \in \SS$
The condition $(1)$, for each $j \in J$, comes down to:
:$\sequence {S_{j_i} }_{j_i \mathop \in J_i} \in \SS^{J_i}$
It follows that $\SS$ satisfies the requirement on $\phi_i$ to be a magma of sets, for each $i \in I$.
That is to say, $\SS$ is a magma of sets for $\Phi$.
{{qed}}
Category:Magmas of Sets
5hf20kl74j2xghvpwc8hvcogj1mdod9
Theorem: Sigma-Algebra as Magma of Sets

The concept of $\sigma$-algebra is an instance of a magma of sets.

Proof:
It will suffice to define partial mappings such that the axiom for a magma of sets crystallises into the axioms for a $\sigma$-algebra.
Let $X$ be any set, and let $\powerset X$ be its power set.
Let $I$ be an index set.
For $S \in \powerset X$, define:
:$\phi_1: \powerset X \to \powerset X: \map {\phi_1} S := X$
:$\phi_2: \powerset X \to \powerset X: \map {\phi_2} S := X \setminus S$
:$\phi_3: \powerset X^\N \to \powerset X: \map {\phi_3} {\sequence {S_n}_{n \mathop \in \N} } := \ds \bigcup_{n \mathop \in \N} S_n$
It is blatantly obvious that $\phi_1, \phi_2$ and $\phi_3$ capture the axioms for a $\sigma$-algebra.
{{finish|Bladibladiblabla, i.e. show that they are mappings, and that the MoS property translates into the $\sigma$-axiom}}
{{tidy|Use the correct link format and standard {{ProofWiki}} notation}}
Let $I$ be the closed (real) interval $[1, 3]$.
For every $i \in I = [1, 3]$, let $J_i = \N$ be the index set, and let:
:$\phi_i: \powerset X^\N \to \powerset X$
be a partial mapping.
We have:
:$X \in \SS$
{{Explain|Why? A link to the proof is required}}
Also:
:$X \setminus S \in \SS$
{{Explain|Why? A link to the proof is required}}
From Union of Subsets is Subset/Subset of Power Set, we have:
:$\ds \bigcup_{n \mathop \in \N} S_n \in \SS$
{{mistake|grammar. Sentences do not begin with "and", at least not in this context. And make your links compliant.}}
It follows that for every indexed family $\family {S_n}_{n \mathop \in \N} \in \SS^{\N}$ in the domain of $\phi_i$ for every $i \in I$:
:$\forall i \in [1, 3]: \map {\phi_i} {\family {S_n}_{n \mathop \in \N} } \in \SS$
It follows that $\SS$ is closed under $\phi_i$ for all $i \in I$.
So $\SS$ is a '''magma of sets for $\set {\phi_i: i \in I}$ on $X$'''
Hence the result.
{{qed}}
Category:Sigma-Algebras
Category:Magmas of Sets
mt0dinelvipynri0hbo88fvidsi2suq
Theorem: Ordinal Multiplication is Closed

Let $x$ and $y$ be ordinals.
Let $\On$ denote the class of all ordinals.
:$x \cdot y \in \On$

Proof:
The proof proceeds by transfinite induction on $y$.
Theorem: Natural Number Multiplication is Closed

Let $m$ and $n$ be natural numbers.
Then:
:$m \times n \in \N$
where $\times$ denotes natural number multiplication.

Proof:
Let $g: \N \to \N$ be defined by:
:$\map g n = m + n$
Applying the Principle of Recursive Definition to $0$ and $g$, we get the following function $f: \N \to \N$:
:$\map f n = \begin{cases} 0 & : n = 0 \\ m + \map f k & : n = k + 1 \end{cases}$
which is seen to be equivalent to $m \times n$ for all $m,n \in \N$.
Hence $m \times n \in \N$.
{{qed}}
Theorem: Ordinal Multiplication by Zero

Let $x$ be an ordinal.
{{begin-eqn}}
{{eqn | l = x \cdot \O
      | r = \O
      | c = 
}}
{{eqn | l = \O \cdot x
      | r = \O
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = x \cdot \O
      | r = \O
      | c = {{Defof|Ordinal Multiplication}}
}}
{{end-eqn}}
For $\O \cdot x = \O$, the proof shall proceed by Transfinite Induction on $x$.
Theorem: Ordinal Multiplication by One

Let $x$ be an ordinal.
Let $1$ denote the ordinal one.
{{begin-eqn}}
{{eqn | l = x \cdot 1
      | r = x
}}
{{eqn | l = 1 \cdot x
      | r = x
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = x \cdot 1
      | r = x \cdot \O^+
      | c = {{Defof|One (Ordinal)}}
}}
{{eqn | r = \paren {x \cdot \O} + x
      | c = {{Defof|Ordinal Multiplication}}
}}
{{eqn | r = \O + x
      | c = {{Defof|Ordinal Multiplication}}
}}
{{eqn | r = x
      | c = Ordinal Addition by Zero
}}
{{end-eqn}}
{{qed|lemma}}
The proof of the other equality shall proceed by Transfinite Induction.
Theorem: Ordinal Addition/Examples/Ordinal Addition by One

Let $x$ be an ordinal.
Let $x^+$ denote the successor of $x$.
Let $1$ denote (ordinal) one, the successor of the zero ordinal $\O$.
Then:
:$x + 1 = x^+$
where $+$ denotes ordinal addition.

Proof:
{{begin-eqn}}
{{eqn | l = x + 1
      | r = x + \O^+
      | c = {{Defof|One (Ordinal)|(ordinal) $1$}}
}}
{{eqn | r = \paren {x + \O}^+
      | c = {{Defof|Ordinal Addition}}
}}
{{eqn | r = x^+
      | c = Ordinal Addition by Zero
}}
{{end-eqn}}
{{qed}}
Theorem: Closed Set Measurable in Borel Sigma-Algebra

Let $\struct {S, \tau}$ be a topological space.
Let $\map \BB \tau$ be the associated Borel $\sigma$-algebra.
Let $C$ be a closed set in $\struct {S, \tau}$.
Then $C$ is $\map \BB \tau$-measurable.

Proof:
Since $C$ is closed, $S \setminus C$ is open.
By definition of Borel $\sigma$-algebra, $S \setminus C \in \map \BB \tau$.
By axiom $(2)$ for $\sigma$-algebras:
:$S \setminus \paren {S \setminus C} \in \map \BB \tau$
and this set equals $C$ by Set Difference with Set Difference since $C \subseteq S$.
The result follows by definition of measurable set.
{{qed}}
Category:Borel Sigma-Algebras
Category:Closed Sets
48u5tup6yq5q86m1ncicbsc437y2714
Theorem: Euler Phi Function preserves Divisibility

:$d \divides n \implies \map \phi d \divides \map \phi n$
where $d \divides n$ denotes that $d$ is a divisor of $n$.

Proof:
Let $d \divides n$.
We can write $n$ as $n = d p_1 p_2 p_3 \cdots p_r$, where $p_1, p_2, \ldots, p_r$ are all the primes (not necessarily distinct) which divide $\dfrac n d$.
Thus, repeatedly using Euler Phi Function of Product with Prime:
{{begin-eqn}}
{{eqn | l = \map \phi d
      | o = \divides
      | r = \map \phi {d p_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \phi {d p_1}
      | o = \divides
      | r = \map \phi {d p_1 p_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \phi {d p_1 p_2}
      | o = \divides
      | r = \map \phi {d p_1 p_2 p_3}
      | c = 
}}
{{eqn | ll= \leadsto
      | o = \cdots
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \phi {d p_1 p_2 \cdots p_{r - 1} }
      | o = \divides
      | r = \map \phi {d p_1 p_2 \cdots p_{r - 1} p_r}
      | c = 
}}
{{end-eqn}}
As the last expression is $\map \phi n$, the result follows from Divisor Relation on Positive Integers is Partial Ordering.
{{qed}}
Category:Euler Phi Function
gaf16afs9orzxul0phku8ayz4qe8tpf
Theorem: Commutative B-Algebra is Entropic Structure

Let $\struct {G, *}$ be a commutative $B$-algebra.
Then $\struct {G, *}$ is an entropic structure.

Proof:
From Commutative $B$-Algebra Induces Abelian Group we have that there exists an abelian group $\struct {G, \circ}$ such that:
:$\forall a, b \in G: a \circ b^{-1} = a * b$ 
where $a * b$ is defined by the binary operation in $\struct {G, *}$.
From Abelian Group Induces Entropic Structure, we have directly that $\struct {G, *}$ is an entropic structure.
{{qed}}
Category:B-Algebras
Category:Entropic Structures
bwl0a88ker0i4o7i42cpwt5h10ejqrr
Theorem: Commutative B-Algebra Induces Abelian Group

Let $\left({X, \circ }\right)$ be a commutative $B$-algebra.
Let $*$ be the binary operation on $X$ defined as:
:$\forall a, b \in X: a * b := a \circ \left({0 \circ b}\right)$
Then the algebraic structure $\left({X, *}\right)$ is an abelian group such that:
:$\forall x \in X: 0 \circ x$ is the inverse element of $x$ under $*$.
That is:
:$\forall a, b \in X: a * b^{-1} := a \circ b$

Proof:
From B-Algebra Induces Group, the algebraic structure $\left({X, *}\right)$ is a group such that:
:$\forall x \in X: 0 \circ x$ is the inverse element of $x$ under $*$.
It remains to show that $*$ is a commutative operation.
Let $x, y \in X$:
{{begin-eqn}}
{{eqn | l=x * y
      | r=x \circ \left({0 \circ y}\right)
      | c=by definition of $*$
}}
{{eqn | r=y \circ \left({0 \circ x}\right)
      | c=by definition of commutative $B$-algebra
}}
{{eqn | r=y * x
      | c=by definition of $*$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Membership is Left Compatible with Ordinal Multiplication

Let $x$, $y$, and $z$ be ordinals.
Then:
:$\paren {x < y \land z > 0} \iff \paren {z \cdot x} < \paren {z \cdot y}$

Proof:
=== Sufficient Condition ===
The proof of the sufficient condition shall proceed by Transfinite Induction on $y$.
{{qed|lemma}}
Theorem: Ordinal Multiplication is Left Cancellable

Let $x, y, z$ be ordinals.
Let $z \ne 0$.
Then:
:$\ds \paren {z \cdot x} = \paren {z \cdot y} \implies x = y$
That is, ordinal multiplication is left cancellable.

Proof:
For the proof, $<$, $\in$, and $\subsetneq$ will be used interchangeably.
This is justified by Transitive Set is Proper Subset of Ordinal iff Element of Ordinal.
Since $z \ne 0$ and $z \not < 0$, $0 < z$ by Ordinal Membership is Trichotomy.
Note that:
{{begin-eqn}}
{{eqn | l = x < y \land z > 0
      | o = \implies
      | r = \paren {z \cdot x} < \paren {z \cdot y}
      | c = Membership is Left Compatible with Ordinal Multiplication
}}
{{eqn | l = y < x \land z > 0
      | o = \implies
      | r = \paren {z \cdot y} < \paren {z \cdot x}
      | c = Membership is Left Compatible with Ordinal Multiplication
}}
{{end-eqn}}
In addition:
{{begin-eqn}}
{{eqn | l = \paren {z \cdot x} = \paren {z \cdot y}
      | o = \implies
      | r = \paren {z \cdot x} \not < \paren {z \cdot y} \land \paren {z \cdot y} \not < \paren {z \cdot x}
      | c = No Membership Loops
}}
{{end-eqn}}
This contradicts the consequents of the first two equations, so:
{{begin-eqn}}
{{eqn | o = \leadsto
      | r = x \not < y \land y \not < x
      | c = Rule of Transposition, Praeclarum Theorema
}}
{{eqn | o = \leadsto
      | r = x = y
      | c = Ordinal Membership is Trichotomy
}}
{{end-eqn}}
{{qed}}
Theorem: Subset is Right Compatible with Ordinal Multiplication

Let $x, y, z$ be ordinals.
Then:
:$x \le y \implies \paren {x \cdot z} \le \paren {y \cdot z}$

Proof:
The proof shall proceed by Transfinite Induction on $z$.
Theorem: Ordinals have No Zero Divisors

Let $x$ and $y$ be ordinals.
Then:
:$\paren {x \cdot y} = 0 \iff \paren {x = 0 \lor y = 0}$

Proof:
=== Necessary Condition ===
Suppose that $\paren {x \cdot y} = 0$ and that $x \ne 0$.
By Ordinal Multiplication by Zero:
: $\paren {x \cdot 0} = 0$
Therefore:
: $\paren {x \cdot y} = \paren {x \cdot 0}$
Thus, by Ordinal Multiplication is Left Cancellable, we have that $y = 0$.
{{qed|lemma}}
Theorem: Sigma-Algebra Closed under Union/Corollary

Let $A_1, \ldots, A_n \in \Sigma$.
Then $\ds \bigcup_{k \mathop = 1}^n A_k \in \Sigma$.

Proof:
Define for $k \in \N, k > n: A_k = \O$.
Then by Sigma-Algebra Contains Empty Set, axiom $(3)$ of a $\sigma$-algebra applies.
Hence:
:$\ds \bigcup_{k \mathop \in \N} A_k = \bigcup_{k \mathop = 1}^n A_k \in \Sigma$
{{qed}}
Category:Sigma-Algebras
lp4zopmk2bg2sfnv9r613ojhqz3lmda
Theorem: Measure is Subadditive/Corollary

Let $E_1, \ldots, E_n \in \Sigma$.
Then:
:$\ds \map \mu {\bigcup_{k \mathop = 1}^n E_k} \le \sum_{k \mathop = 1}^n \map \mu {E_k}$.

Proof:
We have Measure is Subadditive.
The result follows by an application of Finite Union of Sets in Subadditive Function.
{{qed}}
Category:Measure is Subadditive
mzzr5mjrak44ofvq192b71j3b7l43k5
Theorem: Convergence in Norm Implies Convergence in Measure

Let $\struct {X, \Sigma, \mu}$ be a measure space, and let $p \in \R, p \ge 1$.
Let $\sequence {f_n}_{n \mathop \in \N}, f_n : X \to \R$ be a sequence of $p$-integrable functions.
Also, let $f: X \to \R$ be a $p$-integrable function.
Suppose that $f_n$ converges in norm to $f$ (in the $L^p$-norm).
Then $f_n$ converges in measure to $f$ (in $\mu$).
That is:
:$\ds \operatorname {\LL^{\textit p}-\!\lim\,} \limits_{n \mathop \to \infty} f_n = f \implies \operatorname {\mu-\!\lim\,} \limits_{n \mathop \to \infty} f_n = f$

Proof:
Let $\epsilon > 0$.
Then:
{{begin-eqn}}
{{eqn | l = \map \mu {\set {x \in X : \size {\map {f_n} x - \map f x} \ge \epsilon } }
      | r = \map \mu {\set {x \in X : \size {\map {f_n} x - \map f x}^p \ge \epsilon^p } }
}}
{{eqn | o = \le
      | r = \frac{1}{\epsilon^p} \int \size {f_n - f}^p \rd \mu
      | c = Markov's Inequality
}}
{{eqn | o = \to
      | r = 0
      | c = as $n \to +\infty$
}}
{{end-eqn}}
Theorem: Pointwise Convergence Implies Convergence in Measure on Finite Measure Space

Let $\struct {X, \Sigma, \mu}$ be a finite measure space.
Let $\sequence {f_n}_{n \mathop \in \N}, f_n : X \to \R$ be a sequence of measurable functions.
Also, let $f: X \to \R$ be a measurable function.
Suppose that $f$ is the pointwise limit of the $f_n$ $\mu$-almost everywhere.
Then $f_n$ converges in measure to $f$ (in $\mu$).
That is:
:$\ds \lim_{n \mathop \to \infty} \map {f_n} x \stackrel {a.e.} {=} \map f x \implies \operatorname {\mu-\!\lim\,} \limits_{n \mathop \to \infty} f_n = f$

Proof:
Since $\sequence {f_n}_{n \mathop \in \N}$ converges almost everywhere, we have: 
:$\set {x \in X : \sequence {\map {f_n} x}_{n \mathop \in \N} \text { does not converge to } \map f x}$ is a $\mu$-null set.
We aim to deduce that: 
:$\ds \lim_{n \mathop \to \infty} \map \mu {\set {x \in X : \size {\map {f_n} x - \map f x} > \epsilon} } = 0$
for each $\epsilon > 0$. 
Let $\epsilon > 0$.
For each $n \in \N$, define: 
:$A_n = \set {x \in X : \size {\map {f_n} x - \map f x} > \epsilon}$
Also define: 
:$\ds B_n = \bigcup_{k \mathop = n}^\infty A_n$
for each $n \in \N$. 
Then $\sequence {B_n}_{n \mathop \in \N}$ is a decreasing sequence. 
Since $\mu$ is finite, $\map \mu {B_1} < \infty$.
So, from Measure of Limit of Decreasing Sequence of Measurable Sets, we have: 
:$\ds \map \mu {\bigcap_{n \mathop = 1}^\infty B_n} = \lim_{n \mathop \to \infty} \map \mu {B_n}$
Note that if:
:$\ds x \in \bigcap_{n \mathop = 1}^\infty B_n$
We have: 
:$\size {\map {f_n} x - \map f x} > \epsilon$ for each $n \in \N$.
So:
:$\sequence {\map {f_n} x}_{n \mathop \in \N}$ does not converge to $\map f x$. 
So:
:$\ds \bigcap_{n \mathop = 1}^\infty B_n \subseteq \set {x \in X : \sequence {\map {f_n} x}_{n \mathop \in \N} \text { does not converge to } \map f x}$
So, from Null Sets Closed under Subset, we have: 
:$\ds \map \mu {\bigcap_{n \mathop = 1}^\infty B_n} = 0$
and so:
:$\ds \lim_{n \mathop \to \infty} \map \mu {B_n} = 0$ 
That is:
:$\ds \lim_{n \mathop \to \infty} \map \mu {\bigcup_{k \mathop = n}^\infty A_k} = 0$
From Set is Subset of Union, we have: 
:$\ds A_n \subseteq \bigcup_{k \mathop = n}^\infty A_k$ 
So from Measure is Monotone, we have: 
:$\ds 0 \le \map \mu {A_n} \le \map \mu {B_n}$ for each $n \in \N$.
Then, from the Squeeze Theorem for Real Sequences, we have: 
:$\ds \lim_{n \mathop \to \infty} \map \mu {A_n} = 0$
That is: 
:$\ds \lim_{n \mathop \to \infty} \map \mu {\set {x \in X : \size {\map {f_n} x - \map f x} > \epsilon} } = 0$
Since $\epsilon > 0$ was arbitrary, we have:
:$f_n \stackrel \mu \longrightarrow f$
{{qed}}