avewright/proofwiki-math huggingface dataset:
Theorem: Lexicographic Product of Family of Ordered Sets is Ordered Set

Let $\struct {I, \preceq}$ be a well-ordered set.
For each $i \in I$, let $\struct {S_i, \preccurlyeq_i}$ be an ordered set.
Let $\ds D = \prod_{i \mathop \in I} S_i$ be the Cartesian product of the family $\family {\struct {S_i, \preccurlyeq_i} }_{i \mathop \in I}$ indexed by $I$.
Let $\preccurlyeq_D$ be the lexicographic order on $D$, defined as:
:$\forall u, v \in D: u \preccurlyeq_D v \iff \begin {cases} u = v \\ \map u i \preccurlyeq_i \map v i & \text {for the $\preceq$-smallest $i \in I$ such that $\map u i \ne \map v i$} \end {cases}$
Then $\struct {D, \preccurlyeq_D}$ is an ordered set.

Proof:
For a subset $J$ of $I$, let $D_J$ be defined as:
:$\ds D_J = \prod_{i \mathop \in J} S_i$
Similarly, let $\preccurlyeq_J$ be the lexicographic order on $D_J$:
:$\forall u, v \in D_J: u \preccurlyeq_J v \iff \begin {cases} u = v \\ \map u i \preccurlyeq_i \map v i & \text {for the $\preceq$-smallest $i \in J$ such that $\map u i \ne \map v i$} \end {cases}$
Let $Y$ be the subset of $I$ defined as:
:$\ds Y = \leftset {y \in I: \struct {D_Y, \preccurlyeq_Y} }$ is an ordered set $\rightset{}$
We require to show that $Y = I$.
Let $b \in I$ be the smallest element of $I$.
Let $J = \set b$.
We have that:
{{begin-eqn}}
{{eqn | l = D_J
      | r = \prod_{i \mathop \in J} S_i
      | c = 
}}
{{eqn | r = S_b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \preccurlyeq_J
      | r = \preccurlyeq_b
      | c = 
}}
{{end-eqn}}
We have that $\struct {S_b, \preccurlyeq b}$ is an ordered set.
Thus $b \in Y$ by definition of $Y$.
Let $s \in I$ such that:
:$\forall t \in I: t \prec s \implies t \in Y$
Let $T = \set {t \in I: t \prec s}$.
We have that $T \subseteq I$ such that:
:$\struct {D_T, \preccurlyeq_T}$ is an ordered set.
Now we consider the lexicographic product $D_T \otimes^l S_s$.
By Lexicographic Order is Ordering:
:$\struct {D_T \times S_s, \preccurlyeq l}$ is an ordered set.
We have that $\preccurlyeq l$ is defined as:
:$\tuple {u, s_1} \preccurlyeq_l \tuple {v, s_2} \iff \tuple {u \prec_T v} \lor \paren {u = v \land s_1 \preccurlyeq_s s_2}$
But $\preccurlyeq_T$ is defined as:
:$\forall u, v \in D_T: u \preccurlyeq_T v \iff \begin {cases} u = v \\ \map u i \preccurlyeq_i \map v i & \text {for the $\preceq$-smallest $i \in T$ such that $\map u i \ne \map v i$} \end {cases}$
Let $T' = T \cup \set s$.
We see that $\preccurlyeq l$ is the same as:
:$\forall u, v \in D_{T'}: u \preccurlyeq_{T'} v \iff \begin {cases} u = v \\ \map u i \preccurlyeq_i \map v i & \text {for the $\preceq$-smallest $i \in T'$ such that $\map u i \ne \map v i$} \end {cases}$
That is:
:$s \in Y$
Thus we have shown that:
:$\paren {\forall t \in I: t \prec s \implies t \in Y} \implies s \in Y$
By Induction on Well-Ordered Set it follows that $Y = I$.
The result follows.
{{qed}}
{{Proofread}}
{{Improve|There has to be a less tortuous way of using Induction on Well-Ordered Set to prove this. I'm missing something obvious.}}
Theorem: Lexicographic Order of Family of Totally Ordered Sets is Totally Ordered Set

Let $\struct {I, \preceq}$ be a well-ordered set.
For each $i \in I$, let $\struct {S_i, \preccurlyeq_i}$ be a totally ordered set.
Let $\ds D = \prod_{i \mathop \in I} S_i$ be the Cartesian product of the family $\family {\struct {S_i, \preccurlyeq_i} }_{i \mathop \in I}$ indexed by $I$.
Let $\preccurlyeq_D$ be the lexicographic order on $D$, defined as:
:$\forall u, v \in D: u \preccurlyeq_D v \iff \begin {cases} u = v \\ \map u i \preccurlyeq_i \map v i & \text {for the $\preceq$-smallest $i \in I$ such that $\map u i \ne \map v i$} \end {cases}$
Then $\struct {D, \preccurlyeq_D}$ is a totally ordered set.

Proof:
From Lexicographic Product of Family of Ordered Sets is Ordered Set, $\struct {D, \preccurlyeq_D}$ is an ordered set.
It remains to be shown that $\struct {D, \preccurlyeq_D}$ is totally ordered.
Let $p, q \in D$.
If $p = q$, then $p \preccurlyeq_D q$ by the definition of ordering.
If $p \ne q$, then the set $M = \set {i \in I: p_i \ne q_i}$ is non-empty.
Because $\struct {I, \preceq}$ is a well-ordered set and $M \subseteq I$, $M$ has a $\preceq$-least element $k$.
Because $\preccurlyeq_k$ is a total ordering, it must hold that $p_k \preccurlyeq_k q_k$ or $q_k \preccurlyeq_k p_k$.
But:
:$p_k \preccurlyeq_k q_k \implies p \preccurlyeq_D q$
and:
:$q_k \preccurlyeq_k p_k \implies q \preccurlyeq_D p$
so $\preccurlyeq_D$ is a total ordering.
{{qed}}
Theorem: Lexicographic Order of Family of Well-Ordered Sets is not necessarily Well-Ordered

Let $\struct {I, \preceq}$ be a well-ordered set.
For each $i \in I$, let $\struct {S_i, \preccurlyeq_i}$ be a well-ordered set.
Let $\ds D = \prod_{i \mathop \in I} S_i$ be the Cartesian product of the family $\family {\struct {S_i, \preccurlyeq_i} }_{i \mathop \in I}$ indexed by $I$.
Let $\preccurlyeq_D$ be the lexicographic order on $D$, defined as:
:$\forall u, v \in D: u \preccurlyeq_D v \iff \begin {cases} u = v \\ \map u i \preccurlyeq_i \map v i & \text {for the $\preceq$-smallest $i \in I$ such that $\map u i \ne \map v i$} \end {cases}$
Then it is not necessarily the case that $\struct {D, \preccurlyeq_D}$ is also a well-ordered set.

Proof:
Proof by Counterexample:
Let $\struct {I, \preceq} = \struct {\N, \le}$.
Let $\struct {S_i, \preccurlyeq_i} = \struct {\N, \le}$ for all $i \in \N$.
Let $n \in \N$.
Let $\ds u_n \in \prod_{i \mathop \in \N} \N$ be the mapping defined as:
:$\map {u_n} i = \begin {cases} 0 & : i \le n \\ 1 & : i > n \end {cases}$
It is to be shown that the instances of $u_n$ form an infinite decreasing sequence in $\ds {\bigotimes_{i \mathop \in \N} }^l \N$.
Let $\sequence S$ be the sequence of elements of $\prod_{i \mathop \in \N} \N$ defined as:
:$s_i = \sequence {\map {u_n} i}$
We have that:
:$s_i$ starts with $i - 1$ instances of $0$
:$s_{i + 1}$ starts with $i$ instances of $0$.
Hence $s_i$ and $s_{i + 1}$ are first different at that $i$th element.
Further:
:the $i$th element of $s_i$ is $1$
:the $i$th element of $s_{i + 1}$ is $0$
and so by definition of the lexicographic order:
:$s_{i + 1} \preccurlyeq_l s_i$
We have that the terms of $\sequence S$ form a non-empty subset of $\ds \prod_{i \mathop \in \N} \N$ which has no minimal element by $\preccurlyeq_l$.
Hence by Infinite Sequence Property of Well-Founded Relation, $\preccurlyeq_l$ is not well-founded and so is not a well-ordering.
{{qed}}
Theorem: Ordering is Preordering

Let $S$ be a set.
Let $\RR$ be an ordering on $S$.
Then $\RR$ is also a preordering on $S$.

Proof:
By definition of ordering:
{{:Definition:Ordering/Definition 1}}
By definition of preordering:
{{:Definition:Preordering/Definition 1}}
Thus an ordering is a preordering which is antisymmetric.
{{qed}}
Theorem: Preordering is not necessarily Ordering

Let $S$ be a set.
Let $\RR$ be a preordering on $S$.
Then it is not necessarily the case that $\RR$ is also an ordering on $S$.

Proof:
Consider the relation $\RR$ on the powerset of the natural numbers:
:$\forall a, b \in \powerset \N: a \mathrel \RR b \iff a \setminus b \text { is finite}$
where $\setminus$ denotes set difference.
It is demonstrated in Preordering Example: Finite Set Difference on Natural Numbers that;
:$\RR$ is a preordering on $\powerset \N$
but:
:$\RR$ is not an ordering on $\powerset \N$.
{{qed}}
Theorem: Uniformly Continuous Function to Complete Metric Space has Unique Continuous Extension to Closure of Domain

Let $\tuple {X, d}$ be a metric space.
Let $\tuple {Y, d'}$ be a complete metric space.
Let $A \subseteq X$. 
Let $f : A \to Y$ be a uniformly continuous function.
Then there exists a unique continuous function $g : A^- \to Y$ such that:
:$\map g a = \map f a$
for all $a \in A$, where $A^-$ denotes the topological closure of $A$. 
Furthermore, $g$ is uniformly continuous.

Proof:
=== Existence ===
Note that if $A$ is closed, then from Set is Closed iff Equals Topological Closure, we have: 
:$A^- = A$
So taking $g = f$ suffices in this case.
Suppose now that $A$ is not closed.
Theorem: Uniformly Continuous Function to Complete Metric Space has Unique Continuous Extension to Closure of Domain/Lemma 1

Let $\sequence {a_n}$ be a sequence in $A$ convergent to $a \in A^-$. 
Then $\sequence {\map f {a_n} }$ converges.

Proof:
From Set is Closed iff Equals Topological Closure, $A^- \setminus A$ is non-empty. 
Let $a \in A^- \setminus A$. 
From Point in Closure of Subset of Metric Space iff Limit of Sequence:
:there exists a sequence $\sequence {a_n}$ in $A$ converging to $a$.
Consider now the sequence $\sequence {\map f {a_n} }$ in $Y$.
Note that since $Y$ is complete, if we can show that $\sequence {\map f {a_n} }$ is a Cauchy sequence, then we know that it converges.
We therefore want to show that there exists an $N$ such that for $n, m > N$ we have:
:$\map {d'} {\map f {a_n}, \map f {a_m} } < \epsilon$
Since $f$ is uniformly continuous, we can find $\delta > 0$ such that: 
:$\map {d'} {\map f {a_n}, \map f {a_m} } < \epsilon$
whenever: 
:$\map d {a_n, a_m} < \delta$
Since $\sequence {a_n}$ is a Cauchy sequence, we can find $N$ such that for $n, m > N$ we have: 
:$\map d {a_n, a_m} < \delta$
giving:
:$\map {d'} {\map f {a_n}, \map f {a_m} } < \epsilon$
for $n, m > N$. 
So $\sequence {\map f {a_n} }$ is a Cauchy sequence, and so is convergent.
{{qed}}
Category:Uniformly Continuous Function to Complete Metric Space has Unique Continuous Extension to Closure of Domain
hsb0u0kml82c3epr58dqgekkd8gw71x
Theorem: Uniformly Continuous Function to Complete Metric Space has Unique Continuous Extension to Closure of Domain/Lemma 2

Let $\sequence {a_n}$ be a convergent sequence in $A$. 
Then the limit of $\sequence {\map f {a_n} }$ is dependent only on the limit of $\sequence {a_n}$. 
That is, there exists a function $L : A^- \to Y$ such that: 
:$\ds \lim_{n \mathop \to \infty} \map f {a_n} = \map L {\lim_{n \mathop \to \infty} a_n}$
for every convergent sequence $\sequence {a_n}$.

Proof:
Let $\sequence {a_n}$ and $\sequence {b_n}$ be sequences in $A$ such that $a_n \to a$ and $b_n \to a$, with: 
:$\map f {a_n} \to L_1$
and:
:$\map f {b_n} \to L_2$
We have, by the Triangle Inequality:
:$\map {d'} {\map f {a_n}, L_2} \le \map {d'} {\map f {a_n}, \map f {b_n} } + \map {d'} {\map f {b_n}, L_2}$
We want to show that we can find $K$ such that: 
:$\map {d'} {\map f {a_n}, L_2} < \epsilon$
for $n > K$. 
Note that since $f$ is uniformly continuous, we can find $\delta_1$ such that for: 
:$\map d {a_n, b_n} < \delta_1$
we have:
:$\map {d'} {\map f {a_n}, \map f {b_n} } < \dfrac \epsilon 2$
By the Triangle Inequality, we can write: 
:$\map d {a_n, b_n} \le \map d {a_n, a} + \map d {a, b_n}$
Since $a_n \to a$ and $b_n \to a$, we can find $K_1, K_2$ such that for $n > K_1$ we have: 
:$\map d {a_n, a} < \dfrac {\delta_1} 2$
and for $n > K_2$ we have: 
:$\map d {b_n, a} < \dfrac {\delta_1} 2$
So, for $n > \max \set {K_1, K_2}$, we have: 
:$\map d {a_n, b_n} < \delta$
and so:
:$\map {d'} {\map f {a_n}, \map f {b_n} } < \dfrac \epsilon 2$
for $n > \max \set {K_1, K_2}$.
Since $\map f {b_n} \to L_2$, we can pick $K_3$ such that: 
:$\map {d'} {\map f {b_n}, L_2} < \dfrac \epsilon 2$
for $n > K_3$. 
So, setting $K = \max \set {K_1, K_2, K_3}$, we have: 
:$\map {d'} {\map f {b_n}, L_2} < \dfrac \epsilon 2$
for $n > K$.
So:
:$\map {d'} {\map f {a_n}, L_2} < \epsilon$
for $n > K$. 
So $\map f {a_n} \to L_2$.
From Convergent Sequence in Metric Space has Unique Limit, we have:
:$L_1 = L_2$
So, if $a_n \to a$, the sequence $\sequence {\map f {a_n} }$ converges to some limit $\map L a$ dependent only on $a$.
{{qed}}
Category:Uniformly Continuous Function to Complete Metric Space has Unique Continuous Extension to Closure of Domain
qo13y68iac3y7ud7i4gvvmj56vko6st
Theorem: Preordering induces Ordering

Let $\struct {S, \RR}$ be a relational structure such that $\RR$ is a preordering.
Let $\sim_\RR$ denote the equivalence on $S$ induced by $\RR$:
:$x \sim_\RR y$ {{iff}} $x \mathrel \RR y$ and $y \mathrel \RR x$
Let $\preccurlyeq_\RR$ be the relation defined on the quotient set $S / {\sim_\RR}$ by:
:$\eqclass x {\sim_\RR} \preccurlyeq_\RR \eqclass y {\sim_\RR} \iff x \mathrel \RR y$
where $\eqclass x {\sim_\RR}$ denotes the equivalence class of $x$ under $\sim_\RR$.
Then $\preccurlyeq_\RR$ is an '''ordering'''.

Proof:
First we note from Ordering Induced by Preordering is Well-Defined that $\preccurlyeq_\RR$ is a well-defined relation.
Checking in turn each of the criteria for an ordering:
Theorem: Norm on Bounded Linear Transformation is Finite

<onlyinclude>
Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \norm {\, \cdot \,}_X}$ and $\struct {Y, \norm {\, \cdot \,}_Y}$ be normed vector spaces over $\GF$.
Let $A: X \to Y$ be a bounded linear transformation.
Let $\norm A$ denote the norm of $A$ defined by:
:$\norm A = \inf \set {c > 0: \forall h \in X : \norm {A x}_Y \le c \norm x_X}$
Then:
:$\norm A < \infty$

Proof:
By definition of a bounded linear transformation:
:$\exists c \in \R_{> 0}: \forall x \in X : \norm{A x}_Y \le c \norm x_X$
Hence:
:$\set {\lambda > 0: \forall x \in X : \norm {A x}_Y \le \lambda \norm x_X} \ne \O$
By definition:
:$\set {\lambda > 0: \forall x \in X : \norm {A x}_Y \le \lambda \norm x_X}$ is bounded below.
From the Greatest Lower Bound Property:
:$\norm A = \inf \set {\lambda > 0: \forall x \in X : \norm {A x}_Y \le \lambda \norm x_X}$ exists.
We have:
{{begin-eqn}}
{{eqn | l = \norm A
      | o = \le
      | r = c
      | c = {{Defof|Infimum}}
}}
{{eqn | o = <
      | r = \infty
      | c = As $c \in \R_{> 0}$
}}
{{end-eqn}}
The result follows.
{{qed}}
Category:Norm on Space of Bounded Linear Transformations
lp7ybtyobk40ko9nwiyacxkfhm9iihi
Theorem: Mapping on Total Ordering reflects Transitivity

Let $\struct {S, \preccurlyeq}$ be a totally ordered set.
Let $f: S \to T$ be a mapping to an arbitrary set $T$.
Let $\RR$ be a relation on $T$ defined such that:
:$\RR: = \set {\tuple {\map f x, \map f y}: x \preccurlyeq y}$
That is, $a$ is related to $b$ in $T$ {{iff}} they have preimages $x$ and $y$ under $f$ such that $x$ precedes $y$.
Then $\RR$ is transitive.

Proof:
Let $a, b, c \in T$ such that:
:$a \mathrel \RR b$
:$b \mathrel \RR c$
Then there exist $x, y, z \in S$ such that:
:$a = \map f x$
:$b = \map f y$
:$c = \map f z$
such that:
:$x \preccurlyeq y$
:$y \preccurlyeq z$
As $\preccurlyeq$ is a total ordering, it follows that:
:$x \preccurlyeq z$
and so by definition of $\RR$:
:$\map f x \mathrel \RR \map f z$
That is:
:$a \mathrel \RR c$
As $a$, $b$ and $c$ were arbitrary, it follows that $\RR$ is transitive.
{{qed}}
Theorem: Surjection on Total Ordering reflects Preordering

Let $\struct {S, \preccurlyeq}$ be a totally ordered set.
Let $f: S \to T$ be a mapping to an arbitrary set $T$.
Let $\RR$ be a relation on $T$ defined such that:
:$\RR: = \set {\tuple {\map f x, \map f y}: x \preccurlyeq y}$
That is, $a$ is related to $b$ in $T$ {{iff}} they have preimages $x$ and $y$ under $f$ such that $x$ precedes $y$.
Then:
:$f$ is a surjection onto set $T$
{{iff}}:
:$\RR$ is a preordering on $T$

Proof:
=== Sufficient Condition ===
Let $f: S \to T$ be a surjection.
By definition, a preordering is a relation which is both transitive and reflexive.
From Mapping on Total Ordering reflects Transitivity, $\RR$ is a transitive relation.
It remains to be shown that $\RR$ is a reflexive relation.
Let $a \in T$.
Because $f$ is a surjection, it follows that:
:$\exists x \in S: a = \map f x$
Because $\preccurlyeq$ is a total ordering on $S$, it follows that:
:$x \preccurlyeq x$
Hence by definition of $\RR$:
:$\map f x \mathrel \RR \map f x$
That is:
:$a \mathrel \RR a$
As $a$ was arbitrary, it follows that $\RR$ is reflexive.
Hence it follows that $\RR$ is a preordering.
{{qed}}
Theorem: Bijection on Total Ordering reflects Total Ordering

Let $\struct {S, \preccurlyeq}$ be a totally ordered set.
Let $f: S \to T$ be a mapping to an arbitrary set $T$.
Let $\RR$ be a relation on $T$ defined such that:
:$\RR: = \set {\tuple {\map f x, \map f y}: x \preccurlyeq y}$
That is, $a$ is related to $b$ in $T$ {{iff}} they have preimages $x$ and $y$ under $f$ such that $x$ precedes $y$.
Then:
:$f$ is a bijection
{{iff}}:
:$\RR$ is a total ordering.

Proof:
=== Sufficient Condition ===
Let $f$ be a bijection.
Then $f$ is {{afortiori}} a surjection.
Hence from Surjection on Total Ordering reflects Preordering it follows that $\RR$ is a preordering.
A total ordering is a preordering which is also antisymmetric and connected.
Hence it remains to be shown that:
:$\RR$ is antisymmetric
:$\RR$ is connected.
Theorem: Bijection on Total Ordering is Order Isomorphism

Let $\struct {S, \preccurlyeq}$ be a totally ordered set.
Let $f: S \to T$ be a bijection to an arbitrary set $T$.
Let $\RR$ be a relation on $T$ defined such that:
:$\RR: = \set {\tuple {\map f x, \map f y}: x \preccurlyeq y}$
Then $f$ is an order isomorphism between $\struct {S, \preccurlyeq}$ and $\struct {T, \RR}$.

Proof:
From Bijection on Total Ordering reflects Total Ordering, we have that $\RR$ is a total ordering.
We have that $f$ is a bijection.
Hence a fortiori $f$ is also a surjection.
Let $x, y \in S$ such that $x \preccurlyeq y$.
Then by definition of $\RR$:
:$\map f x \mathrel \RR \map f y$
Now let $\map f x \mathrel \RR \map f y$.
Then again by definition of $\RR$:
:$x \preccurlyeq y$
That is, $f$ is by definition an order isomorphism between $\struct {S, \preccurlyeq}$ and $\struct {T, \RR}$.
{{qed}}
Theorem: Mapping from Preordering reflects Ordering

Let $\struct {S, \RR}$ be a preordered set.
Then there exists:
:an ordered set $\struct {T, \preccurlyeq}$
:a mapping $f: S \to T$ such that:
::$\RR: = \set {\tuple {x, y}: \map f x \preccurlyeq \map f y}$

Proof:
Let $\sim_\RR$ denote the equivalence on $S$ induced by $\RR$:
:$x \sim_\RR y$ {{iff}} $x \mathrel \RR y$ and $y \mathrel \RR x$
Let $\preccurlyeq_\RR$ be the ordering on the quotient set $S / {\sim_\RR}$ by $\RR$:
:$\eqclass x {\sim_\RR} \preccurlyeq_\RR \eqclass y {\sim_\RR} \iff x \mathrel \RR y$
where $\eqclass x {\sim_\RR}$ denotes the equivalence class of $x$ under $\sim_\RR$.
Let $f: S \to S / {\sim_\RR}$ be the quotient mapping induced by $\RR$:
:$\forall x \in S: \map f x = \eqclass x \RR$
From Preordering induces Ordering we have that $\struct {T, \preccurlyeq}$ is an set with exactly the properties required.
{{qed}}
Theorem: Set is Equivalent to Itself

Let $S$ be a set.
Then:
:$S \sim S$
where $\sim$ denotes set equivalence.

Proof:
From Identity Mapping is Bijection, the identity mapping $I_S: S \to S$ is a bijection from $S$ to $S$.
Thus there exists a bijection from $S$ to itself
Hence by definition $S$ is therefore equivalent to itself.
Theorem: Set Equivalence behaves like Equivalence Relation/Symmetric

Set equivalence behaves like a symmetric relation:
:$S \sim T \implies T \sim S$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = S \sim T
      | c = 
}}
{{eqn | o = \leadsto
      | r = \exists \phi: S \to T
      | c = {{Defof|Set Equivalence}}, where $\phi$ is a bijection
}}
{{eqn | o = \leadsto
      | r = \exists \phi^{-1}: T \to S
      | c = Bijection iff Inverse is Bijection
}}
{{eqn | o = \leadsto
      | r = T \sim S
      | c = {{Defof|Set Equivalence}}: $\phi^{-1}$ is also a bijection
}}
{{end-eqn}}
Theorem: Set Equivalence behaves like Equivalence Relation/Transitive

Set equivalence behaves like a transitive relation:
:$S_1 \sim S_2 \land S_2 \sim S_3 \implies S_1 \sim S_3$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = S_1 \sim S_2 \land S_2 \sim S_3
      | c = 
}}
{{eqn | o = \leadsto
      | r = \exists \phi_1: S_1 \to S_2 \land \exists \phi_2: S_2 \to S_3
      | c = {{Defof|Set Equivalence}}: $\phi_1$ and $\phi_2$ are bijections
}}
{{eqn | o = \leadsto
      | r = \exists \phi_2 \circ \phi_1: S_1 \to S_3
      | c = Composite of Bijections is Bijection: $\phi_2 \circ \phi_1$ is a bijection
}}
{{eqn | o = \leadsto
      | r = S_1 \sim S_3
      | c = {{Defof|Set Equivalence}}
}}
{{end-eqn}}
Theorem: Collection of Sets Equivalent to Set Containing Empty Set is Proper Class

Let $S = \set \O$ be the singleton whose element is the empty set.
Let $C$ be the collection of all sets which are equivalent to $S$.
$C$ is a proper class.

Proof:
By definition of cardinality, $C$ is the collection of all singletons:
:$\set {x: \exists y: x = \set y}$
Define a class mapping $f: C \to V$, where $V$ is the universal class, such that $\map f {\set x} = x$.
This is a mapping on the domain $C$, as all elements of $C$ are singletons.
Take an arbitrary $y \in V$.
Then by definition of $C$:
:$\set y \in C$
and by definition of $f$: 
:$\map f {\set y} = y$
Thus:
:$\exists x \in A: \map f x = y$
and $f$ is a surjection.
From Universal Class is Proper, $V$ is proper.
It follows from Surjection from Class to Proper Class that $C$ is proper.
{{qed}}
Theorem: Finite Set of Continuous Functions between Metric Spaces is Pointwise Equicontinuous

Let $\struct {X, d}$ and $\struct {Y, d'}$ be metric spaces. 
Let $\map \CC {X, Y}$ be the set of continuous functions $X \to Y$.
Let $\FF = \set {f_1, f_2, \ldots, f_n}$ be a finite subset of $\map \CC {X, Y}$.
Then $\FF$ is pointwise equicontinuous.

Proof:
Let $x \in X$.
Let $\epsilon \in \R_{>0}$.
Let $i$ be a natural number with $1 \le i \le n$. 
Since $f_i$ is continuous at $x$, there exists $\delta_i > 0$ such that whenever: 
:$\map d {x, y} < \delta_i$
we have:
:$\map {d'} {\map {f_i} x, \map {f_i} y} < \epsilon$
Let:
:$\ds \delta = \min_i \set {\delta_i}$
so that: 
:$\delta \le \delta_i$
for each $i$. 
Then, whenever:
:$\map d {x, y} < \delta$
we have: 
:$\map {d'} {\map {f_i} x, \map {f_i} y} < \epsilon$
for each $i$.
So $\FF$ is pointwise equicontinuous.
{{qed}}
Category:Pointwise Equicontinuity
tllj8d6iednud3dzppoz9pov1aejwu9
Theorem: Ordering of Cardinality of Sets is Well-Defined

The relation $\le$ in the context of cardinalities of sets is well-defined in the sense that:
:if $\card A = \card {A'}$ and $\card B = \card {B'}$, then there exists an injection from $A$ into $B$ {{iff}} there exists an injection from $A'$ into $B'$.

Proof:
{{ProofWanted|I'm losing interest -- I'm going to work on something else for a bit.}}
Theorem: Symmetric Group is Generated by Transposition and n-Cycle

Let $n \in \Z: n > 1$.
Let $S_n$ denote the symmetric group on $n$ letters.
Then the set of cyclic permutations:
:$\set {\begin {pmatrix} 1 & 2 \end{pmatrix}, \begin {pmatrix} 1 & 2 & \cdots & n \end{pmatrix} }$
is a generator for $S_n$.

Proof:
Denote:
:$s = \begin {pmatrix} 1 & 2 \end{pmatrix}$
:$r = \begin {pmatrix} 1 & 2 & \cdots & n \end{pmatrix}$
By Cycle Decomposition of Conjugate,:
:$r s r^{-1} = r \begin {pmatrix} 1 & 2 \end{pmatrix} r^{-1} = \begin {pmatrix} \map r 1 & \map r 2 \end{pmatrix} = \begin {pmatrix} 2 & 3 \end{pmatrix}$.
By repeatedly using Cycle Decomposition of Conjugate:
:$r^2 s r^{-2} = \begin {pmatrix} 3 & 4 \end{pmatrix}$
:$r^3 s r^{-3} = \begin {pmatrix} 4 & 5 \end{pmatrix}$
:$\cdots$
:$r^{n - 2} s r^{-\paren {n - 2} } = \begin {pmatrix} n - 1 & n \end{pmatrix}$
The result then follows from Transpositions of Adjacent Elements generate Symmetric Group.
{{qed}}