avewright/proofwiki-math huggingface dataset:
Theorem: Ordered Field of Rational Cuts is Isomorphic to Rational Numbers

Let $\struct {\RR, +, \times, \le}$ denote the ordered field of rational cuts.
Let $\struct {\Q, +, \times, \le}$ denote the field of rational numbers.
Then $\struct {\RR, +, \times, \le}$ and $\struct {\Q, +, \times, \le}$ are isomorphic.

Proof:
{{ProofWanted|Straightforward but tedious}}
Theorem: Supremum of Subset of Real Numbers May or May Not be in Subset

Let $S \subset \R$ be a proper subset of the set $\R$ of real numbers.
Let $S$ admit a supremum $M$.
Then $M$ may or may not be an element of $S$.

Proof:
Consider the subset $S$ of the real numbers $\R$ defined as:
:$S = \set {\dfrac 1 n: n \in \Z_{>0} }$
It is seen that:
:$S = \set {1, \dfrac 1 2, \dfrac 1 3, \ldots}$
and hence $\sup S = 1$.
Thus $\sup S \in S$.
Consider the subset $T$ of the real numbers $\R$ defined as:
:$T = \set {-\dfrac 1 n: n \in \Z_{>0} }$
It is seen that:
:$T = \set {-1, -\dfrac 1 2, -\dfrac 1 3, \ldots}$
and hence $\sup T = 0$.
Thus $\sup T \notin T$.
{{Qed}}
Theorem: Infimum of Subset of Real Numbers May or May Not be in Subset

Let $S \subset \R$ be a proper subset of the set $\R$ of real numbers.
Let $S$ admit an infimum $m$.
Then $m$ may or may not be an element of $S$.

Proof:
Consider the subset $S$ of the real numbers $\R$ defined as:
:$S = \set {\dfrac 1 n: n \in \Z_{>0} }$
It is seen that:
:$S = \set {1, \dfrac 1 2, \dfrac 1 3, \ldots}$
and hence $\inf S = 0$.
Thus $\inf S \notin S$.
Consider the subset $T$ of the real numbers $\R$ defined as:
:$T = \set {-\dfrac 1 n: n \in \Z_{>0} }$
It is seen that:
:$T = \set {-1, -\dfrac 1 2, -\dfrac 1 3, \ldots}$
and hence $\inf T = 1$.
Thus $\inf T \in T$.
{{Qed}}
Theorem: Uniqueness of Positive Root of Positive Real Number/Positive Exponent

Let $x \in \R$ be a real number such that $x > 0$.
Let $n \in \Z$ be an integer such that $n > 0$.
Then there is at most one $y \in \R: y \ge 0$ such that $y^n = x$.

Proof:
We have that:
:$0 < y_1 < y_2 \implies y_1^n < y_2^n$
so there exists at most one $y \in \R: y \ge 0$ such that $y^n = x$.
{{Qed}}
Theorem: Uniqueness of Positive Root of Positive Real Number/Positive Exponent

Let $x \in \R$ be a real number such that $x > 0$.
Let $n \in \Z$ be an integer such that $n > 0$.
Then there is at most one $y \in \R: y \ge 0$ such that $y^n = x$.

Proof:
To prove uniqueness, we must show that:
:$y_1^n = x = y_2^n$ implies $y_1 = y_2$
{{AimForCont}} that $y_1 \ne y_2$.
Then $y_1 < y_2$ or $y_2 < y_1$.
{{WLOG}}, assume that $y_1 < y_2$.
We will show by induction that $y_1^n < y_2^n$, contradicting the assumption that $y_1^n = x = y_2^n$.
=== Basis for the Induction ===
By assumption:
:$y_1^1 < y_2^1$
This is our basis for the induction.
=== Induction Hypothesis ===
We need to show that $y_1^n < y_2^n$ implies $y_1^{n + 1} < y_2^{n + 1}$.
So this is our induction hypothesis:
:$y_1^n < y_2^n$
=== Induction Step ===
By the induction hypothesis, $y_1^n < y_2^n$.
By assumption, both $y_1$ and $y_2$ are positive, giving the following choices:
:$y_1^n = 0 \quad \text{and} \quad y_2^n > 0$
:$y_1^n > 0 \quad \text{and} \quad y_2^n > 0$
The first case violates our assumption that $y_1^n = x = y_2^n$.
Assume the second case:
:$y_1^n > 0 \quad y_2^n > 0$
Then by the Real Number Axioms and our assumption that $y_1 < y_2$, the following hold:
:$y_1^n \cdot y_1 < y_2^n \cdot y_1$
:$y_2^n \cdot y_1 < y_2^n \cdot y_2$
This gives:
:$y_1^{n + 1} < y_2^{n + 1}$
completing the proof by induction.
{{qed|lemma}}
Thus $y_1^n \ne y_2^n$, contradicting our assumption.
Therefore, for strictly positive $n \in \Z$ and $x \in \R$, there is a unique positive $y \in \R$ such that $y^n=x$.
{{Qed}}
Theorem: Existence and Uniqueness of Positive Root of Positive Real Number/Positive Exponent

Let $x \in \R$ be a real number such that $x \ge 0$.
Let $n \in \Z$ be an integer such that $n > 0$.
Then there always exists a unique $y \in \R: \paren {y \ge 0} \land \paren {y^n = x}$.

Proof:
=== Proof of Existence ===
{{:Existence of Positive Root of Positive Real Number/Positive Exponent}}
Theorem: Basis Condition for Coarser Topology

Let $S$ be a set.
Let $\BB_1$ and $\BB_2$ be two bases on $S$.
Let $\tau_1$ and $\tau_2$ be the topologies generated by $\BB_1$ and $\BB_2$ respectively.
If $\BB_1$ and $\BB_2$ satisfy:
:$\forall U \in \BB_1 : \exists \AA \subseteq \BB_2: U = \bigcup \AA$
then $\tau_1$ is coarser than $\tau_2$.

Proof:
Let $\BB_1$ and $\BB_2$ satisfy:
:$\forall U \in \BB_1 : \exists \AA \subseteq \BB_2: U = \bigcup \AA$
Let $U \in \BB_1$.
Then there exists $\AA_2 \subseteq \BB_2$ such that $U = \bigcup \AA_2$.
By definition of the topology generated by $\BB_2$, it follows that $U \in \tau_2$.
Since $U$ was arbitrary, it follows that $\BB_1 \subseteq \tau_2$.
Let $W \in \tau_1$.
By definition of the topology generated by $\BB_1$:
:there exists $\AA_1 \subseteq \BB_1$ such that $W = \bigcup \AA_1$.
Since $\BB_1 \subseteq \tau_2$, it follows that $\AA_1 \subseteq \tau_2$.
By the open set axiom $(O1)$, then $W \in \tau_2$.
Since $W$ was arbitrary, it follows that $\tau_1 \subseteq \tau_2$.
The result follows.
{{qed}}
Category:Topology
i8n1euif1ypip5nhwejfujlsrjpged1
Theorem: Basis Condition for Coarser Topology/Corollary 1

If $\BB_1$ and $\BB_2$ satisfy:
:$\forall U \in \BB_1: \forall x \in U: \exists V \in \BB_2: x \in V \subseteq U$
then $\tau_1$ is coarser than $\tau_2$.

Proof:
Let $\BB_1$ and $\BB_2$ satisfy:
:$\forall U \in \BB_1: \forall x \in U: \exists V \in \BB_2: x \in V \subseteq U$
Let $U \in \BB_1$.
Let $\AA = \set {V \in \BB_2 : V \subseteq U}$
From Union of Family of Sets is Smallest Superset:
:$\bigcup \AA \subseteq V$
Let $x \in U$.
Then:
:$\exists V_x \in \BB_2 : x \in V_x \subseteq U$
Thus:
:$V_x \in \AA$
and
:$x \in V_x \subseteq \bigcup \AA$
Since $x$ was arbitrary, it follows that:
:$U \subseteq \bigcup \AA$
By the definition of set equality:
:$U = \bigcup \AA$
Since $U$ was arbitrary, it follows that $\BB_1$ and $\BB_2$ satisfy:
:$\forall U \in \BB_1 : \exists \AA \subseteq \BB_2: U = \bigcup \AA$
From Basis Condition for Coarser Topology, $\tau_1$ is coarser than $\tau_2$.
{{qed}}
Category:Topology
1zhb26tgjsjt1fduu2m276b0j0lvc7r
Theorem: Basis Condition for Coarser Topology/Corollary 2

If $\BB_1 \subseteq \BB_2$ then $\tau_1$ is coarser than $\tau_2$.

Proof:
Let $\BB_1 \subseteq \BB_2$.
Let $U \in \BB_1$.
Let $\AA = \set U$.
Then:
:$\AA \subseteq \BB_2$
and
:$U = \bigcup \AA$
So:
:$\forall U \in \BB_1 : \exists \AA \subseteq \BB_2: U = \bigcup \AA$
From Basis Condition for Coarser Topology:
:$\tau_1$ is coarser than $\tau_2$
{{qed}}
Category:Topology
gmwsn3hqv1yry5z79x0w8txvwssvsli
Theorem: Continuous Mapping on Finer Domain and Coarser Codomain Topologies is Continuous

Let $\struct {X, \tau_1}$ and $\struct {Y, \tau_2}$ be topological spaces.
Let $f: \struct {X, \tau_1} \to \struct {Y, \tau_2}$ be a continuous mapping.
Let $\tau'_1$ be a finer topology on $X$ than $\tau_1$, that is, $\tau_1 \subseteq \tau'_1$.
Let $\tau'_2$ be a coarser topology on $Y$ than $\tau_2$, that is, $\tau'_2 \subseteq \tau_2$.
Then:
:$f: \struct {X, \tau'_1} \to \struct {Y, \tau'_2}$ is a continuous mapping.

Proof:
Let $U \in \tau'_2$.
Since $\tau'_2$ is a coarser topology than $\tau_2$:
:$U \in \tau_2$
By definition of continuity:
:$\map {f^{-1}} U \in \tau_1$
Since $\tau'_1$ is a finer topology than $\tau_1$:
:$\map {f^{-1}} U \in \tau'_1$
Since $U$ was arbitrary, by definition of continuity:
:$f: \struct {X, \tau'_1} \to \struct {Y, \tau'_2}$ is a continuous mapping
{{qed}}
Category:Topology
e1qsjh48v81uxnduhrf29bekhv9qwob
Theorem: Projection from Box Topology is Continuous

Let $\family {\struct{X_i, \tau_i}}_{i \mathop \in I}$ be an $I$-indexed family of topological spaces.
Let $X$ be the cartesian product of $\family {X_i}_{i \mathop \in I}$, that is:
:$\ds X := \prod_{i \mathop \in I} X_i$
Let $\tau$ be the box topology on $X$.
For each $i \in I$, let $\pr_i: X \to X_i$ denote the $i$th projection on $X$:
:$\forall \family {x_j}_{j \mathop \in I} \in X: \map {\pr_i} {\family {x_j}_{j \mathop \in I} } = x_i$
Then $\pr_i: \struct {X, \tau} \to \struct {X_i, \tau_i}$ is continuous for all $i \in I$.

Proof:
Let $\tau'$ be the product topology on $X$.
From Projection from Product Topology is Continuous:
:$\forall i \in I : \pr_i : \struct{X, \tau'} \to \struct{X_i, \tau_i}$ is continuous
From Box Topology contains Product Topology, $\tau$ is a finer topology than $\tau'$ on $X$.
From Continuous Mapping on Finer Domain and Coarser Codomain Topologies is Continuous, 
:$\forall i \in I : \pr_i : \struct {X, \tau} \to \struct{X_i, \tau_i}$ is continuous
{{qed}}
Category:Box Topology
oe35tgelnt3njtv46xmzpam5fk6bglk
Theorem: Domain Topology Contains Initial Topology iff Mappings are Continuous

Let $\struct{Y, \tau}$ be a topological space.
Let $\family {\struct{X_i, \tau_i}}_{i \mathop \in I}$ be a family of topological spaces.
Let $\family {f_i}_{i \mathop \in I}$ be a family of mappings $f_i : Y \to X_i$.
Let $\tau'$ be the initial topology on $Y$ with respect to $\family {f_i}_{i \mathop \in I}$.
Then:
:$\tau' \subseteq \tau$ {{iff}} $\forall i \in I : f_i: \struct{Y, \tau} \to \struct{X_i, \tau_i}$ is $\tuple{\tau, \tau_i}$-continuous.

Proof:
=== Necessary Condition ===
Let $\tau' \subseteq \tau$.
From Equivalence of Definitions of Initial Topology:
:for each $i \in I$, $f_i: \struct{Y, \tau'} \to \struct{X_i, \tau_i}$ is $\tuple{\tau', \tau_i}$-continuous
From Continuous Mapping on Finer Domain and Coarser Codomain Topologies is Continuous:
:for each $i \in I$, $f_i: \struct{Y, \tau} \to \struct{X_i, \tau_i}$ is $\tuple{\tau, \tau_i}$-continuous
{{qed|lemma}}
Theorem: Final Topology Contains Codomain Topology iff Mappings are Continuous

Let $\struct{Y, \tau}$ be a topological space.
Let $\family {\struct{X_i, \tau_i}}_{i \mathop \in I}$ be a family of topological spaces.
Let $\family {f_i}_{i \mathop \in I}$ be a family of mappings $f_i : X_i \to Y$.
Let $\tau'$ be the final topology on $Y$ with respect to $\family {f_i}_{i \mathop \in I}$.
Then:
:$\tau \subseteq \tau'$ {{iff}} $\forall i \in I : f_i: \struct{X_i, \tau_i} \to \struct{Y, \tau}$ is continuous.

Proof:
=== Necessary Condition ===
Let $\tau \subseteq \tau'$.
From Equivalence of Definitions of Final Topology:
:for each $i \in I$, $f_i: \struct{X_i, \tau_i} \to \struct{Y, \tau'}$ is $\tuple{\tau_i, \tau'}$-continuous
From Continuous Mapping on Finer Domain and Coarser Codomain Topologies is Continuous:
:for each $i \in I$, $f_i: \struct{X_i, \tau_i} \to \struct{Y, \tau}$ is $\tuple{\tau_i, \tau}$-continuous
{{qed|lemma}}
Theorem: Equivalence of Definitions of Final Topology

Let $X$ be a set.
Let $I$ be an indexing set.
Let $\family {\struct {Y_i, \tau_i} }_{i \mathop \in I}$ be an indexed family of topological spaces indexed by $I$.
Let $\family {f_i: Y_i \to X}_{i \mathop \in I}$ be an indexed family of mappings indexed by $I$.
{{TFAE|def = Final Topology}}

Proof:
=== Definition 1 Implies Definition 2 ===
{{:Equivalence of Definitions of Final Topology/Definition 1 Implies Definition 2}}{{qed|lemma}}
Theorem: Condition for Trivial Relation to be Mapping

Let $S$ and $T$ be sets.
Let $\RR = S \times T$ be the trivial relation in $S$ to $T$.
Then $\RR$ is a mapping {{iff}} either:
:$(2): \card S = 0$
or:
:$(1): \card T = 1$
where $\card {\, \cdot \,}$ denotes cardinality.

Proof:
By definition, the trivial relation in $S$ to $T$ is the set:
:$\RR = \set {\tuple {s, t}: s \in S, t \in T}$
Proof by Cases:
:$(1)$: Let $\card S = 0$.
That is, $S = \O$.
By definition of the trivial relation, in this case $\RR = \O$.
This is the empty mapping.
From Empty Mapping is Mapping, this is a mapping.
:$(2)$: Let $\card S \ne 0$.
That is, $S \ne \O$.
::$(2) \, \text (a)$: Let $\card T = 0$.
That is, $T = \O$.
From Relation to Empty Set is Mapping iff Domain is Empty, $\RR$ cannot be a mapping for $S \ne \O$.
::$(2) \, \text (b)$: Let $\card T = 1$.
So, let $T = \set t$.
Then the trivial relation in $S$ to $T$ is:
:$\RR = \set {\tuple {s, t}: s \in S}$
We have that each element of $S$ is associated with exactly one element of $T$.
Hence $\RR$ is a mapping by definition.
::$(2) \, \text (c)$: Let $\card T > 1$.
Then:
:$\exists t_1, t_2 \in T: t_1 \ne t_2$
We have that $S \ne \O$, so $\exists s \in S$.
Thus by definition of trivial relation:
:$\tuple {s, t_1} \in \RR$
and:
:$\tuple {s, t_2} \in \RR$
but $t_1 \ne t_2$.
Thus $\RR$ is not a mapping.
Hence the result.
{{qed}}
Theorem: Relation to Empty Set is Mapping iff Domain is Empty

Let $S$ be a set
Let $S \times \O$ denote the cartesian product of $S$ with the empty set $\O$.
Let $\RR \subseteq S \times \O$ be a relation in $S$ to $\O$.
Then $\RR$ is a mapping {{iff}} $S = \O$.

Proof:
Let $S \ne \O$.
Then $\exists s \in S$.
But there exists no $t \in \O$.
Hence there is no $\tuple {s, t} \in \RR$.
So $\RR$ is not a mapping by definition.
Let $S = \O$.
Then $\RR$ is the empty mapping by definition.
From Empty Mapping is Mapping, it is demonstrated that $\RR$ is indeed a mapping.
Hence the result.
{{qed}}
Category:Empty Mapping
Category:Relation Theory
n0kf18xiynpzlp7ojd6oqm8zy9zuiff
Theorem: Equivalence of Definitions of Initial Topology/Definition 1 Implies Definition 2

Let:
:$\SS = \set{\map {f_i^{-1}} U: i \in I, U \in \tau_i} \subseteq \powerset X$
where $\map {f_i^{-1}} U$ denotes the preimage of $U$ under $f_i$.
Let $\tau$ be the topology on $X$ generated by the subbase $\SS$.

Proof:
==== Mappings are Continuous ====
Let $i \in I$.
Let $U \in \tau_i$.
Then $\map {f_i^{-1} } U$ is an element of the subbase $\SS$ of $X$, and is therefore trivially in $\tau$.
{{qed|lemma}}
==== $\tau$ is the Coarsest such Topology ====
Let $\struct {X, \vartheta}$ be a topological space.
Let the mappings $\family {f_i: X \to Y_i}_{i \mathop \in I}$ be $\tuple {\vartheta, \tau_i}$-continuous.
Let $U \in \SS$.
Then for some $i \in I$ and some $V \in \tau_i$:
:$U = \map {f_i^{-1} } V$
By definition of the continuity of $f_i$:
:$U \in \vartheta$
From Equivalence of Definitions of Topology Generated by Synthetic Sub-Basis:
:$\tau \in \vartheta$
That is, $\tau$ is coarser than $\vartheta$.
Theorem: Equivalence of Definitions of Initial Topology/Definition 2 Implies Definition 1

Let $\tau$ be the coarsest topology on $X$ such that each $f_i: X \to Y_i$ is $\tuple{\tau, \tau_i}$-continuous.
Let:
:$\SS = \set {\map {f_i^{-1} } U: i \in I, U \in \tau_i} \subseteq \map \PP X$
where $\map {f_i^{-1} } U$ denotes the preimage of $U$ under $f_i$.

Proof:
Let $\map \tau \SS$ be the topology on $X$ generated  by the subbase $\SS$.
==== $\tau$ contains Topology Generated by $\SS$ ====
Let $i \in I$ and $U \in \tau_i$.
By definition of $\tuple{\tau, \tau_i}$-continuity:
:$\map {f_i^{-1} } U \in \tau$
Since $i \in I$ and $U \in \tau_i$ were arbitrary, then $\SS \subseteq \tau$.
From Equivalence of Definitions of Topology Generated by Synthetic Sub-Basis:
:$\map \tau \SS \subseteq \tau$
{{qed|lemma}}
==== Topology Generated by $\SS$ Contains $\tau$ ====
Let $i \in I$.
Let $U \in \tau_i$.
Then $\map {f_i^{-1} } U$ is an element of the subbase $\SS$ of $X$, and is therefore trivially in $\map \tau \SS$.
By definition of $\tuple{\map \tau \SS, \tau_i}$-continuity:
:each $f_i: X \to Y_i$ is $\tuple{\map \tau \SS, \tau_i}$-continuous
Because $\tau$ is the coarsest topology on $X$ such that each $f_i: X \to Y_i$ is $\tuple{\tau, \tau_i}$-continuous:
:$\tau \subseteq \map \tau \SS$
By definition of set equality:
:$\tau = \map \tau \SS$
Theorem: Even Natural Numbers are Infinite

The set of even natural numbers is infinite.

Proof:
Let $E$ denote the set of even natural numbers.
{{AimForCont}} $E$ is finite.
Then there exists $n \in \N$ such that $E$ has $n$ elements.
Let $m$ be the greatest element of $E$.
But then $m + 2$ is an even natural number.
But $m + 2 > m$, and $m$ is the greatest element of $E$.
Therefore $m + 2$ is an even natural number that is not an element of $E$.
So $E$ does not contain all the even natural numbers.
From that contradiction it follows by Proof by Contradiction that $E$ is not finite.
{{Qed}}
Theorem: Set of Points on Line Segment is Infinite

The set of points on a line segment is infinite.

Proof:
Let $S$ denote the set of points on a line segment.
{{AimForCont}} $S$ is finite.
Then there exists $n \in \N$ such that $S$ has $n$ elements.
Let $s_1$ and $s_2$ be two arbitrary adjacent points in $S$.
That is, such that there are no points in $S$ between $s_1$ and $s_2$.
But there exists (at least) one point on the line segment between $s_1$ and $s_2$ which is not in $S$.
Hence there must be more than $n$ elements of $S$.
From that contradiction it follows by Proof by Contradiction that $S$ is not finite.
{{Qed}}
Theorem: Set of Doubletons of Natural Numbers is Countable

Let $S$ be the set defined as:
:$S = \set {\set {n_1, n_2}: n_1, n_2 \in \N, n_1 \ne n_2}$
where $\N$ denotes the set of natural numbers.
Then $S$ is countably infinite.

Proof:
We can write the elements of $S \times T$ in the form of an infinite table:
:$\begin{array} {*{4}c}
 \tuple {1, 0} &  &  &  \\
 \tuple {2, 0} & \tuple {2, 1} &  & \\
 \tuple {3, 0} & \tuple {3, 1} & \tuple {3, 2} & \\
 \vdots  & \vdots  & \vdots & \ddots \\
\end{array}$
This table clearly contains all the elements of $S$.
Let $\set {n_1, n_2} \in S$ be written such that $n_1 > n_2$.
Then $\set {n_1, n_2}$ will be found in row $n_1$ and column $n_2 + 1$ of the table.
The index of the $n$th row is the $n$th triangular number.
Let $f: S \to \N$ be defined as:
:$\forall \set {n_1, n_2} \in S: \map f {\set {n_1, n_2} } = \dfrac {n_1 \paren {n_1 + 1} } 2 + n_2$
It is seen that $f$ is an injection.
With a little more work it can be shown to be a bijection as well, but that condition  is not necessary.
The result follows.
{{qed}}
Theorem: Finite Sets are Comparable

Let $S$ and $T$ be finite sets.
Then $S$ and $T$ are comparable by size.

Proof:
By definition of finite set, there exist $m, n \in \N$ such that:
:$S \sim \N_{<n}$
:$T \sim \N_{<m}$
That is, there are bijections $f, g$:
:$f: S \to \N_{<n}$
:$g: T \to \N_{<m}$
{{WLOG}}, suppose that $m \le n$.
Then $\N_{<m} \subseteq \N_{<n}$, and so we can define:
:$h: T \to S, \map h t = \map {f^{-1}} { \map g t }$
where $f^{-1}: \N_{<n} \to S$ is the inverse of $f$.
By Inverse of Bijection is Bijection and Composite of Injections is Injection, it follows that $h$ is injective.
By Injection to Image is Bijection, $h$ is a bijection to $\Img h$.
Since $\Img h \subseteq S$, it follows that $T$ is comparable to $S$.
{{qed}}
Theorem: Equivalence of Definitions of Final Topology/Definition 1 Implies Definition 2

Let:
:$\tau = \set{U \subseteq X: \forall i \in I: \map {f_i^{-1}} U \in \tau_i} \subseteq \powerset X$

Proof:
From Final Topology is Topology, $\tau$ is a topology.
==== Mappings are continuous ====
Let $U \in \tau$.
Let $i \in I$.
Then $\map {f_i^{-1}} {U} \in \tau_i$ by definition of $\tau$.
It follows that for each $i \in I$, $f_i: Y_i \to X$ is $\tuple {\tau_i, \tau}$-continuous.
{{qed|lemma}}
==== $\tau$ is the finest such topology ====
Let $\struct{X, \vartheta}$ be a topological space.
Let the mappings $\family {f_i: Y_i \to X}_{i \mathop \in I}$ be $\tuple {\tau_i, \vartheta}$-continuous.
Let $U \in \vartheta$.
By definition of continuity, for every $i \in I$:
:$\map {f_i^{-1} } U \in \tau_i$
Then by definition of $\tau$:
:$U \in \tau$
It follows that:
:$\vartheta \subseteq \tau$
That is, $\tau$ is finer than $\vartheta$.
Theorem: Equivalence of Definitions of Final Topology/Definition 2 Implies Definition 1

Let $\tau$ be the finest topology on $X$ such that each $f_i: Y_i \to X$ is $\tuple{\tau_i, \tau}$-continuous.

Proof:
Let $\tau' =  \set{U \subseteq X: \forall i \in I: \map {f_i^{-1} } U \in \tau_i}$.
==== $\tau'$ contains $\tau$ ====
Let $U \in \tau$.
By definition of  $\tuple {\tau_i, \tau}$-continuity for each $i \in I$:
:$\forall i \in I : \map {f_i^{-1} } U \in \tau_i$
So:
:$U \in \tau'$
Since $U$ was arbitrary:
:$\tau \subseteq \tau'$
{{qed|lemma}}
==== $\tau$ contains $\tau'$ ====
From Final Topology is Topology then $\tau'$ is a topology.
Let $U \in \tau'$.
Let $i \in I$.
Then $\map {f_i^{-1}} {U} \in \tau_i$ by definition of $\tau'$.
It follows that for each $i \in I$, $f_i: Y_i \to X$ is $\tuple{\tau_i, \tau'}$-continuous.
So $\tau'$ is a topology on $X$ such that each $f_i: Y_i \to X$ is $\tuple {\tau_i, \tau'}$-continuous.
Since $\tau$ is the finest topology on $X$ such that each $f_i: Y_i \to X$ is $\tuple {\tau_i, \tau}$-continuous then:
:$\tau' \subseteq \tau$
By definition of set equality:
:$\tau = \tau'$
Theorem: Strictly Positive Integers have same Cardinality as Natural Numbers

Let $\Z_{>0} := \set {1, 2, 3, \ldots}$ denote the set of strictly positive integers.
Let $\N := \set {0, 1, 2, \ldots}$ denote the set of natural numbers.
Then $\Z_{>0}$ has the same cardinality as $\N$.

Proof:
Consider the mapping $f: \N \to \Z_{>0}$ defined as:
:$\forall x \in \N: \map f x = x + 1$
Then $f$ is trivially seen to be a bijection.
The result follows by definition of cardinality.
Theorem: Power Set of Natural Numbers has Cardinality of Continuum

Let $\N$ denote the set of natural numbers.
Let $\powerset \N$ denote the power set of $\N$.
Let $\card {\powerset \N}$ denote the cardinality of $\powerset \N$.
Let $\mathfrak c = \card \R$ denote the cardinality of the continuum.
Then:
:$\mathfrak c = \card {\powerset \N}$

Proof:
=== Outline ===
$\powerset \N$ is demonstrated to have the same cardinality as the set of real numbers.
This is done by identifying a real number with its basis expansion in binary notation.
Such a basis expansion is a sequence of $0$s and $1$s.
Each $1$ of a real number $x$ expressed in such a way can be identified with the integer which identifies the power of $2$ representing the $1$ in that place.
Hence $x$ corresponds to the subset of $\N$ whose elements are the positions in $x$ which hold a $1$.
Thus $\R$ and $\powerset \N$ are equivalent.
From the Cantor-Dedekind Hypothesis, the real numbers are in one-to-one correspondence with the points on a line segment.
The points on a line segment form a continuum.
{{ProofWanted|Formalise the above}}