avewright/proofwiki-math huggingface dataset:
Theorem: Equivalence of Definitions of Matroid Circuit Axioms/Formulation 3 Implies Formulation 1

Let $S$ be a finite set.
Let $\mathscr C$ be a non-empty set of subsets of $S$.
Let $\mathscr C$ satisfy the circuit axioms (formulation 3):
{{:Axiom:Circuit Axioms (Matroid)/Formulation 3}}
Then:
:$\mathscr C$ satisfies the circuit axioms (formulation 1):
{{:Axiom:Circuit Axioms (Matroid)/Formulation 1}}

Proof:
Let $\mathscr C$ satisfy the circuit axioms $(\text C 1)$, $(\text C 2)$ and $(\text C 3'')$.
We need to show that $\mathscr C$ satisfies circuit axiom:
{{begin-axiom}}
{{axiom | n = \text C 3
        | q = \forall C_1, C_2 \in \mathscr C
        | mr = C_1 \ne C_2 \land z \in C_1 \cap C_2 \implies \exists C_3 \in \mathscr C : C_3 \subseteq \paren {C_1 \cup C_2} \setminus \set z
}}
{{end-axiom}}
In fact we prove the contrapositive statement:
{{begin-axiom}}
{{axiom | q = \forall C_1, C_2 \in \mathscr C
        | mr = z \in C_1 \cap C_2 \land \paren{\forall C \in \mathscr C : C \nsubseteq \paren {C_1 \cup C_2} \setminus \set z} \implies C1 = C2
}}
{{end-axiom}}
Let:
:$C_1, C_2 \in \mathscr C$
:$z \in C_1 \cap C_2$
:$\forall C \in \mathscr C : C \nsubseteq \paren{C_1 \cup C_2} \setminus \set z$
From circuit axiom $(\text C 5)$:
:$\exists \text{ at most one } C \in \mathscr C : C \subseteq \paren{\paren{C_1 \cup C_2} \setminus \set z} \cup \set z = C_1 \cup C_2$
From Set is Subset of Union:
:$C_1, C_2 \subseteq C_1 \cup C_2$
Hence:
:$C_1 = C_2$
It follows that $\mathscr C$ satisfies circuit axiom $(\text C 3)$.
Theorem: Equivalence of Definitions of Matroid Circuit Axioms/Formulation 2 Implies Formulation 1

Let $S$ be a finite set.
Let $\mathscr C$ be a non-empty set of subsets of $S$.
Let $\mathscr C$ satisfy the circuit axioms (formulation 2):
{{:Axiom:Circuit Axioms (Matroid)/Formulation 2}}
Then:
:$\mathscr C$ satisfies the circuit axioms (formulation 1):
{{:Axiom:Circuit Axioms (Matroid)/Formulation 1}}

Proof:
Let $\mathscr C$ satisfy the circuit axioms $(\text C 1)$, $(\text C 2)$ and $(\text C 4)$.
We need to show that $\mathscr C$ satisfies circuit axiom:
{{begin-axiom}}
{{axiom | n = \text C 3
        | q = \forall C_1, C_2 \in \mathscr C
        | mr= C_1 \ne C_2 \land z \in C_1 \cap C_2 \implies \exists C_3 \in \mathscr C : C_3 \subseteq \paren {C_1 \cup C_2} \setminus \set z
}}
{{end-axiom}}
Let $C_1, C_2 \in \mathscr C : C_1 \ne C_2$.
Let $z \in C_1 \cap C_2$.
From circuit axiom $(\text C 2)$:
:$C_2 \nsubseteq C_1$
By definition of subset and set difference:
:$\exists w \in C_2 \setminus C_1$
From circuit axiom $(\text C 4)$:
:$\exists C_3 \in \mathscr C : w \in C_3 \subseteq \paren{C_1 \cup C_2} \setminus \set z$
It follows that $\mathscr C$ satisfies circuit axiom $(\text C 3)$.
Theorem: Path Component of Locally Path-Connected Space is Closed

Let $T = \struct {S, \tau}$ be a locally path-connected topological space.
Let $G$ be a path component of $T$.
Then $G$ is open in $T$.

Proof:
Let $x \in \partial G$, where $\partial G$ denotes the boundary of $G$.
By {{Open-set-axiom|3}}, it follows that $S \in \tau$.
As $x \in S$, it follows that $S$ is a neighborhood of $x$.
By definition of locally path-connected space, it follows that there exists a path-connected neighborhood $N$ of $x$ such that $N \subseteq S$.
By definition of boundary, there exists $y \in N$ such that $y \in G$.
As $N$ is path-connected, there exists a path between $x$ and $y$.
By definition of path component , it follows that $x \in G$.
Thus, $\partial G \subseteq G$.
From Set is Closed iff it Contains its Boundary, it follows that $G$ is closed.
{{qed}}
Theorem: Circuits of Matroid iff Matroid Circuit Axioms/Lemma 1

Let $\tuple{x_1, \ldots, x_q}$ be any ordered tuple of elements of $S$.
Let $\pi$ be any permutation of $\tuple{x_1, \ldots, x_q}$.
Then:
:$\map t {x_1, \ldots, x_q} = \map t {x_{\map \pi 1}, \ldots, x_{\map \pi q}}$

Proof:
It is sufficient to show that:
:$\forall 1 \le i \le q-1 : \map t {x_1, \ldots, x_i, x_{i + 1}, \ldots, x_q} = \map t {x_1, \ldots, x_{i + 1}, x_i, \ldots, x_q}$
By definition of $t$, we have:
:$\map t {x_1, \ldots, x_i, x_{i + 1}, \ldots, x_q} = \sum_{j = 1}^{i - 1} \map \theta {x_1, \ldots, x_q}_j + \map \theta {x_1, \ldots, x_q}_i + \map \theta {x_1, \ldots, x_q}_{i + 1} + \sum_{j = {i + 2} }^q \map \theta {x_i + 2, \ldots, x_q}_j$
Similarly:
:$\map t {x_1, \ldots, x_{i + 1}, x_i, \ldots, x_q} = \sum_{j = 1}^{i - 1} \map \theta {x_1, \ldots, x_q}_j + \map \theta {x_1, \ldots, x_q}_{i + 1} + \map \theta {x_1, \ldots, x_q}_i + \sum_{j = {i + 2} }^q \map \theta {x_i + 2, \ldots, x_q}_j$
By definition of $\theta$:
:$\sum_{j = {i + 2} }^q \map \theta {x_i + 2, \ldots, x_q}_j$ is independent of the order of the tuple $\tuple{x_1, \ldots, x_{i - 1}, x_i, x_{i + 1}}$
So it is sufficient to show that:
:$\forall 1 \le i \le q-1 : \map t {x_1, \ldots, x_i, x_{i + 1}} = \map t {x_1, \ldots, x_{i + 1}, x_i}$
Let:
:$a = \map t {x_1, \ldots, x_{i - 1}}$
:$a_1 = \map t {x_1, \ldots, x_{i - 1}, x_i} = a + \map \theta {x_1, \ldots, x_{i - 1}, x_i}_i$
:$a_2 = \map t {x_1, \ldots, x_{i - 1}, x_{i + 1}} = a + \map \theta {x_1, \ldots, x_{i - 1}, x_{i + 1}}_i$
:$a_{12} = \map t {x_1, \ldots, x_{i - 1}, x_i, x_{i + 1}} = a_1 + \map \theta {x_1, \ldots, x_{i - 1}, x_i, x_{i + 1}}_{i+1}$
:$a_{21} = \map t {x_1, \ldots, x_{i - 1}, x_{i + 1}, x_i} = a_2 + \map \theta {x_1, \ldots, x_{i - 1}, x_{i + 1}, x_i}_{i+1}$
We consider the following cases:
:<nowiki>$\begin{array}{c|cccc}
\text{Case} & \map \theta {x_1, \ldots, x_{i - 1}, x_i}_i & \map \theta {x_1, \ldots, x_{i - 1}, x_{i + 1}}_i & \map \theta {x_1, \ldots, x_{i - 1}, x_i, x_{i + 1}}_{i+1} \\
\hline
\text{Case } 1 & 1 & 1 & 1 \\
\text{Case } 2 & 1 & 1 & 0 \\
\text{Case } 3 & 1 & 0 & 1 \\
\text{Case } 4 & 1 & 0 & 0 \\
\text{Case } 5 & 0 & 1 & 1 \\
\text{Case } 6 & 0 & 1 & 0 \\
\text{Case } 7 & 0 & 0 & 1 \\
\text{Case } 8 & 0 & 0 & 0 \\
\end{array}$</nowiki>
Theorem: Circuits of Matroid iff Matroid Circuit Axioms/Lemma 2

Let $X \subseteq S$ and $y \in S \setminus X$.
Then:
:$\map \rho {X \cup \set y} = \map \rho X$ {{iff}} $\exists C \in \mathscr C : y \in C \subseteq X \cup \set y$

Proof:
Let $X = \set{x_1, \ldots, x_q}$
We have:
{{begin-eqn}}
{{eqn | l = \map \rho {X \cup \set y}
      | r = \map t {x_1, \ldots, x_q, y}
      | c = Definition of $\rho$
}}
{{eqn | r = \map t {x_1, \ldots, x_q} + \map \theta {x_1, \ldots, x_q, y}_{q+1}
      | c = Definition of $t$
}}
{{eqn | r = \map \rho X + \map \theta {x_1, \ldots, x_q, y}_{q+1}
      | c = Definition of $t$
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \map \rho {X \cup \set y} = \map \rho X
      | o = \leadstoandfrom
      | r = \map \theta {x_1, \ldots, x_q, y}_{q+1} = 0
}}
{{eqn | o = \leadstoandfrom
      | r = \exists C \in \mathscr C : y \in C \subseteq X \cup \set y
      | c = Definition of $\theta$
}}
{{end-eqn}}
{{qed}}
Category:Circuits of Matroid iff Matroid Circuit Axioms
b6ofud3fz38vzixigir9g3blffvpjze
Theorem: Circuits of Matroid iff Matroid Circuit Axioms/Lemma 3

:$\mathscr C$ is the set of circuits of $M$.

Proof:
Let $\mathscr C_M$ be the set of circuit of the matroid $M$.
Theorem: Circuits of Matroid iff Matroid Circuit Axioms/Lemma 4

:$\forall C \in \mathscr C_M : \exists C' \in \mathscr C : C' \subseteq C$

Proof:
Let $C \in \mathscr C_M$.
By definition of circuit:
:$C$ is dependent
By matroid axiom $(\text I 1)$:
:$C \neq \O$
Let $x \in C$.
From Proper Subset of Matroid Circuit is Independent:
:$C  \setminus \set x$ is independent
We have:
{{begin-eqn}}
{{eqn | l = \map \rho C
      | r = \card C - 1
      | c = Rank of Matroid Circuit is One Less Than Cardinality
}}
{{eqn | r = \card C - \card{\set x}
      | c = Cardinality of Singleton
}}
{{eqn | r = \card {C  \setminus \set x}
      | c = Cardinality of Set Difference
}}
{{eqn | r = \map \rho {C  \setminus \set x}
      | c = Rank of Independent Subset Equals Cardinality
}}
{{end-eqn}}
Theorem: Circuits of Matroid iff Matroid Circuit Axioms/Lemma 5

:$\forall C \in \mathscr C : \exists C' \in \mathscr C_M : C' \subseteq C$

Proof:
Let $C \in \mathscr C$.
From circuit axiom $(\text C 1)$:
:$\exists y \in C$
We have:
:$C \subseteq C = \paren{C \setminus \set y} \cup \set y$
Theorem: Set of Finite Strings is Countably Infinite

Let $\Sigma$ be a finite alphabet.
Let $\Sigma^*$ be the set of finite strings of $\Sigma$.
Then $\Sigma^*$ is a countably infinite set.

Proof:
Let $b = \size \Sigma$, that is, the number of symbols.
Theorem: Power Set of Set of Finite Strings is Uncountable

Let $\Sigma$ be a finite alphabet.
Let $\Sigma^*$ be the set of finite strings of $\Sigma$.
Let $\powerset {\Sigma^*}$ be the power set of $\Sigma^*$
Then $\powerset {\Sigma^*}$ is an uncountable set.

Proof:
From Set of Finite Strings is Countably Infinite, $\Sigma^*$ is a countably infinite set.
The result follows from Power Set of Countably Infinite Set is Uncountable.
{{qed}}
Theorem: Quotient Norm is Norm

Let $\Bbb F \in \set {\R, \C}$. 
Let $\struct {X, \norm {\, \cdot \,} }$ be a normed vector space over $\Bbb F$. 
Let $N$ be a closed linear subspace of $X$.
Let $X/N$ be the quotient vector space of $X$ modulo $N$.
Let $\norm {\, \cdot \,}_{X/N}$ be the quotient norm on $X/N$.
Then $\norm {\, \cdot \,}_{X/N}$ is indeed a norm.

Proof:
=== Norm is Well-Defined and Finite ===
Let $\pi$ be the quotient map associated with $X/N$.
We show that if $x, x' \in X$ have $\map \pi x = \map \pi {x'}$, then: 
:$\ds \inf_{z \mathop \in N} \norm {x - z} = \inf_{z \mathop \in N} \norm {x' - z}$
From Quotient Mapping is Linear Transformation:
:$\map \pi {x' - x} = 0$
From Kernel of Quotient Mapping:
:$x' - x \in N$
Since $N$ is a linear subspace of $X$:
:$\paren {x' - x} + N = N$
So, we may manipulate: 
{{begin-eqn}}
{{eqn	| l = \inf_{z \mathop \in N} \norm {x - z}
		| r = \inf_{z \mathop \in \paren {x' - x} + N} \norm {x - \paren {z - \paren {x' - x} } }
}}
{{eqn	| r = \inf_{z \mathop \in \paren {x' - x} + N} \norm {x' - z}
}}
{{eqn	| r = \inf_{z \mathop \in N} \norm {x' - z}
}}
{{end-eqn}}
and so the quotient norm is well-defined.
Since: 
:$\norm {x - z} \ge 0$
for all $z \in N$, we also have: 
:$\ds \inf_{z \mathop \in N} \norm {x - z} \ge 0$ 
{{qed|lemma}}
Theorem: Quotient Vector Space is Vector Space

Let $K$ be a field.
Let $X$ be a vector space over $K$. 
Let $N$ be a linear subspace of $X$.
Define: 
:$X/N = \set {x + N : x \in X}$
where $x + N$ is the Minkowski sum of $x$ and $N$.
Define: 
:$\paren {x + N} +_{X/N} \paren {y + N} = \paren {x + y} + N$
for $x, y \in X$, and:
:$\alpha \circ_{X/N} {x + N} = \paren {\alpha x} + N$
for $\alpha \in K$ and $x \in X$. 
Then $\paren {X/N, +_{X/N}, \circ_{X/N} }_K$ is a vector space.

Proof:
=== Lemma ===
{{:Quotient Vector Space is Vector Space/Lemma}}{{qed|lemma}}
Theorem: Quotient Mapping is Bounded in Normed Quotient Vector Space

Let $\Bbb F \in \set {\R, \C}$.
Let $X$ be a normed vector space over $\Bbb F$.
Let $N$ be a closed linear subspace of $X$. 
Let $\struct {X/N, \norm {\, \cdot \,}_{X/N} }$ be the normed quotient vector space associated with quotient vector space $X/N$.
Let $\pi : X \to X/N$ be the quotient mapping associated with $X/N$. 
Then $\pi$ is a bounded linear transformation.

Proof:
From Quotient Mapping is Linear Transformation:
:$\pi$ is a linear transformation.
Let $x \in X$. 
Note that from the definition of quotient norm, we have: 
:$\ds \norm {\map \pi x}_{X/N} = \inf_{z \in N} \norm {x - z}_X$
Note that since $0 \in N$, we have that: 
:$\norm x_X \in \set {\norm {x - z}_X : z \in N}$ 
so that: 
:$\ds \inf_{z \in N} \norm {x - z}_X \le \norm x$ 
from the definition of the infimum.
So we have: 
:$\norm {\map \pi x}_{X/N} \le \norm x$ 
for each $x \in X$, and so: 
:$\pi$ is a bounded linear transformation.
{{qed}}
Category:Quotient Mappings
Category:Normed Quotient Vector Spaces
Category:Bounded Linear Transformations
dybjj2mnd6vax6dyj7uv283p2jmb1or
Theorem: Bing's Metrization Theorem

Let $T = \struct {S, \tau}$ be a topological space.
Then:
:$T$ is metrizable {{iff}} $T$ is regular and has a $\sigma$-discrete basis

Proof:
{{proof wanted}}
{{Namedfor|R.H. Bing|cat = Bing}}
Theorem: Cantor's Diagonal Argument/Corollary

Let $S$ be a set such that $\card S > 1$, that is, such that $S$ is not a singleton.
Let $\mathbb G$ be the set of all mappings from the integers $\Z$ to $S$:
:$\mathbb G = \set {f: \Z \to S}$
Then $\mathbb G$ is uncountably infinite.

Proof:
Let $\mathbb F$ be the set of all mappings from the natural numbers $\N$ to $S$:
:$\mathbb F = \set {f: \N \to S}$
From Cantor's Diagonal Argument, $\mathbb F$ is uncountably infinite.
Let $s \in S$ be an arbitrary distinguished element of $S$.
Let $\mathbb H$ be the set of mappings $h: \Z \to S$ defined as:
:$\forall f \in \mathbf F: \forall x \in \Z: \map h x = \begin {cases} \map f x & : x \ge 0 \\ s & : x < 0 \end {cases}$
It can be shown that $\mathbf H$ and $\mathbf F$ are equivalent.
Hence as $\mathbb F$ is uncountable, $\mathbf H$ is likewise uncountable.
We also have that $\mathbf H$ is a subset of $\mathbf G$.
{{AimForCont}} $\mathbf G$ is countable.
Then from Subset of Countable Set is Countable it follows that $\mathbf H$ is countable.
Hence by Proof by Contradiction it follows that $\mathbf G$ is uncountable.
{{qed}}
Category:Cantor's Diagonal Argument
jheejmar7whk1k0wv1678ioene0osqa
Theorem: Quotient Mapping Maps Unit Open Ball in Normed Vector Space to Unit Open Ball in Normed Quotient Vector Space

Let $\struct {X, \norm {\, \cdot \,} }$ be a normed vector space.
Let $N$ be a closed linear subspace of $X$.
Let $\struct {X/N, \norm {\, \cdot \,} }$ be the normed quotient vector space associated with the quotient vector space $X/N$.
Let $B_X$ be the unit open ball in $\struct {X, \norm {\, \cdot \,} }$.
Let $B_{X/N}$ be the unit open ball in $\struct {X/N, \norm {\, \cdot \,} }$.
Let $\pi$ be the quotient mapping associated with $X/N$.
Then:
:$\map \pi {B_X} = B_{X/N}$

Proof:
From Quotient Mapping is Bounded in Normed Quotient Vector Space, we have: 
:$\norm {\map \pi x}_{X/N} \le \norm x$ 
So if $x \in B_X$, we have $\norm x < 1$ and hence: 
:$\norm {\map \pi x}_{X/N} < 1$
So $\map \pi x \in B_{X/N}$.
So we have: 
:$\map \pi {B_X} \subseteq B_{X/N}$
Conversely, let $\mathbf x \in B_{X/N}$ and pick $x \in X$ such that $\mathbf x = \map \pi x$.
Then we have:
:$\norm {\map \pi x}_{X/N} = \inf_{z \in N} \norm {x - z} < 1$ 
So there exists $z_\ast \in N$ such that: 
:$\norm {x - z_\ast} < 1$
so that: 
:$x - z_\ast \in B_X$
From Kernel of Quotient Mapping and Quotient Mapping is Linear Transformation, we have: 
:$\map \pi {x - z_\ast} = \map \pi x = \mathbf x$
So we have: 
:$\mathbf x \in \map \pi {B_X}$ 
So we have: 
:$B_{X/N} \subseteq \map \pi {B_X}$ 
{{qed}}
Category:Quotient Mappings
Category:Normed Quotient Vector Spaces
03l17o1a56kpdx3o5abmkz0mi27carx
Theorem: Characterization of Complete Normed Quotient Vector Spaces

Let $\struct {X, \norm {\, \cdot \,}_X}$ be a normed vector space.
Let $N$ be a closed linear subspace of $X$. 
Let $\struct {X/N, \norm {\, \cdot \,}_{X/N} }$ be the normed quotient vector space associated with the quotient vector space $X/N$.
Let $\norm {\, \cdot \,}_N$ be the norm on $N$ given by restricting the norm on $X$. 
Then $\struct {X, \norm {\, \cdot \,}_X}$ is a Banach space {{iff}} $\struct {N, \norm {\, \cdot \,}_N}$ and $\struct {X/N, \norm {\, \cdot \,}_{X/N} }$ are Banach spaces.

Proof:
Let $\pi : X \to X/N$ be the quotient mapping associated with $X/N$.
Theorem: Bounded Linear Transformation preserves Cauchy Sequences

Let $\struct {X, \norm {\, \cdot \,}_X}$ and $\struct {Y, \norm {\, \cdot \,}_Y}$ be normed vector spaces.
Let $T : X \to Y$ be a bounded linear transformation.
Let $\sequence {x_n}_{n \mathop \in \N}$ be a Cauchy sequence in $X$.
Then $\sequence {T x_n}_{n \mathop \in \N}$ is a Cauchy sequence in $Y$.

Proof:
Since $T$ is a bounded linear transformation, there exists $M > 0$ such that: 
:$\norm {T x}_Y \le M \norm x_X$
for all $x \in X$. 
So, since $T$ is linear, we have:
:$\norm {T x_n - T x_m}_Y \le M \norm {x_n - x_m}_X$
Let $\epsilon > 0$.
Since $\sequence {x_n}_{n \mathop \in \N}$ is Cauchy, there exists $N \in \N$ such that: 
:$\ds \norm {x_n - x_m}_X < \frac \epsilon M$ 
for $n, m \ge N$. 
Then: 
:$\ds \norm {T x_n - T x_m} < M \paren {\frac \epsilon M} = \epsilon$ 
for $n, m \ge N$. 
So $\sequence {T x_n}_{n \mathop \in \N}$ is a Cauchy sequence in $Y$.
{{qed}}
Category:Bounded Linear Transformations
sfa3yhmc1hmcq6w7tugkiu0ie7umi25
Theorem: Number of Atoms in Observable Universe

The number of atoms in the observable universe is approximately $10^{80}$.

Proof:
According to our current observations and understanding of the {{WP|Universe}}, the age of the universe is estimated to be $13.787$ billion years.
That means the light from the most distant galaxies has traveled $13.787$ billion years to reach us.
The speed of light is $299 \, 792 \, 458 \ \text {m s}^{-1}$
This implies that the radius of the observable universe (assuming no expansion) is:
{{begin-eqn}}
{{eqn | l = R_U
      | r = \paren {13.787 \times 10^9 \text { years} } \times \paren {365 \cdotp 24219 \, 878 \text { days per year} } \times \paren { 86 \, 400 \text { seconds per day} } \times \paren {299 \,792 \, 458 \ \text {m s}^{-1} } 
      | c = 
}}
{{eqn | r = 1.304 \times 10^{26} \ \mathrm m 
      | c = 
}}
{{end-eqn}}
However, contemplating expansion at an average rate of $8.8 \%$ per billion years, we obtain:
{{begin-eqn}}
{{eqn | l = R_U
      | r = 1.304 \times 10^{26} \times e^{0.088 \times 13.787} \ \mathrm m
      | c = 
}}
{{eqn | r = 4.39 \times 10^{26} \ \mathrm m 
      | c = 
}}
{{end-eqn}}
This in turn implies that the volume of the observable universe is:
{{begin-eqn}}
{{eqn | l = V_U
      | r = \dfrac {4 \pi {R_U}^3} 3
      | c = Volume of Sphere
}}
{{eqn | r = \dfrac {4 \pi \paren {4.39 \times 10^{26} } \ \mathrm m^3} 3
      | c = 
}}
{{eqn | r = 3.54 \times 10^{80} \ \mathrm m^3
      | c = 
}}
{{end-eqn}}
Finally, assuming there is approximately $1$ atom per cubic metre brings us to our estimate of approximately $10^{80}$ atoms in the observable universe.
{{qed}}
Category:Atoms
evmj4k3jl16s56dyoapgiwo6nycszu3
Theorem: Metrization of Regular Second Countable Space

Let $T = \struct {S, \tau}$ be a $T_1$ space.
{{TFAE}}
:$(1): \quad T$ is regular and second-countable
:$(2): \quad T$ is homeomorphic to a metric subspace of the Hilbert cube $I^\omega$
:$(3): \quad T$ is metrizable and separable

Proof:
=== Condition $(1)$ implies Condition $(2)$ ===
Follows immediately from Regular Second-Countable Space is Homeomorphic to Subspace of Hilbert Cube.
{{qed|lemma}}
Theorem: Equivalence of Definitions of Sine and Cosine

In the following, $\theta$ understood to take values in $\hointr 0 {2 \pi}$.

Proof:
Consider the following vector-valued function $\mathbf f : \R \to {\closedint {-1} 1}^2$:
:$\map {\mathbf f} t = \tuple {\cos t, \sin t}$
where $\cos t$ and $\sin t$ are defined analytically.
Then, for any $t$ the distance to the origin is:
{{begin-eqn}}
{{eqn | l = \norm {\map {\mathbf f} t - \bszero}
      | r = \norm {\map {\mathbf f} t}
}}
{{eqn | r = \sqrt {\cos^2 t + \sin^2 t}
      | c = {{Defof|Euclidean Norm}}
}}
{{eqn | r = 1
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
Therefore, $\map {\mathbf f} t$ always lies on the unit circle.
For arbitrary $\theta \in \hointr 0 {2 \pi}$, the arc length on $\closedint 0 \theta$ is:
{{begin-eqn}}
{{eqn | l = s
      | r = \int_0^\theta \sqrt {\paren {\frac \d {\d t} \cos t}^2 + \paren {\frac \d {\d t} \sin t}^2} \rd t
      | c = Arc Length for Parametric Equations
}}
{{eqn | r = \int_0^\theta \sqrt {\paren {-\sin t}^2 + \paren {\cos t}^2} \rd t
      | c = Derivative of Cosine Function and Derivative of Sine Function
}}
{{eqn | r = \int_0^\theta \rd t
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \theta
      | c = Definite Integral of Constant
}}
{{end-eqn}}
Thus, by the definition of radians, the angle made by $\map {\mathbf f} \theta$ with the $x$-axis is $\theta$.
A straight line segment from $\tuple {0, \sin \theta}$ to $\tuple {\cos \theta, \sin \theta}$ is perpendicular to the $y$-axis.
Its length is $\size {\cos \theta}$, and it is on the side of the $y$-axis corresponding to the sign of $\cos \theta$.
But that is the unit circle definition for cosine.
{{qed|lemma}}
Similarly, a straight line segment from $\tuple {\cos \theta, 0}$ to $\tuple {\cos \theta, \sin \theta}$ is perpendicular to the $x$-axis, with length $\size {\sin \theta}$ and appropriate direction.
Again, that is the unit circle definition for sine.
{{qed}}
Category:Sine Function
Category:Cosine Function
Category:Definition Equivalences
daufaxcw4v01www20t1myzaucub5dhn
Theorem: Construction of Transitive Closure of Relation

Let $\RR$ be a relation.
Let $\RR^+$ be the relation which is constructed from $\RR$ as follows:
:$(1): \quad$ If $\tuple {a, b} \in \RR$, then $\tuple {a, b} \in \RR^+$
:$(2): \quad$ If $\tuple {a, b} \in \RR^+$ and $\tuple {b, c} \in \RR$, then $\tuple {a, c} \in \RR^+$
:$(3): \quad$ Nothing is in $\RR^+$ unless it so follows from $(1)$ and $(2)$.
Then $\RR^+$ is the transitive closure of $\RR$.

Proof:
Let $\tuple {x, y} \in \R^+$ from rules $(1)$ and $(2)$.
Then either:
:$\tuple {x, y}$ belongs there because $\RR \subseteq \RR^+$
or:
:$\tuple {x, y}$ belongs there, because if it were not then $\RR^+$ would not be transitive.
It remains to be shown that $\RR^+$ is in fact transitive.
{{finish|"Easy inductive proof", says H&U, that $\RR^+$ is in fact transitive}}
Because of the method of construction, it follows that $\RR^+$ is the smallest transitive relation on $S$ which contains $\RR$ as a subset.
Theorem: Sub-Basis for Initial Topology in terms of Sub-Bases of Target Spaces

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$.
For each $i \in I$, let $S_i$ be a synthetic basis for $\struct {Y_i, \tau_i}$. 
Let $\family {f_i: X \to Y_i}_{i \mathop \in I}$ be an indexed family of mappings indexed by $I$.
Let $\tau$ be the initial topology on $X$ with respect to $\family {f_i}_{i \mathop \in I}$.
Then: 
:$\SS = \set {f_i^{-1} \sqbrk U : i \in I, \, U \in S_i}$
is a synthetic sub-basis for $\struct {X, \tau}$.

Proof:
Note that by the definition of the initial topology, $\tau$ is generated by the synthetic sub-basis: 
:$\SS' = \set {f_i^{-1} \sqbrk U : i \in I, \, U \in \tau_i}$ 
Since $S_i \subseteq \tau_i$ for each $i \in I$, we have: 
:$\SS \subseteq \SS'$
and hence: 
:$\map \tau \SS \subseteq \map \tau {\SS'} = \tau$
where $\tau$ denotes the generated topology.
Now fix $i \in I$ and $U \in \tau_i$. 
Since $S_i$ is a synthetic sub-basis for $\tau_i$, there exists an indexing set $A$ such that: 
:for each $\alpha \in A$ there exists $n_\alpha \in \N$ and $U_{\alpha, 1}, U_{\alpha, 2}, \ldots, U_{\alpha, n_\alpha}$ such that together: 
::$\ds U = \bigcup_{\alpha \mathop \in A} \, \bigcap_{i \mathop = 1}^{n_\alpha} U_{\alpha, n_\alpha}$
Then we have:
{{begin-eqn}}
{{eqn	| l = f_i^{-1} \sqbrk U
		| r = f_i^{-1} \sqbrk {\bigcup_{\alpha \mathop \in A} \, \bigcap_{i \mathop = 1}^{n_\alpha} U_{\alpha, n_\alpha} }
}}
{{eqn	| r = \bigcup_{\alpha \mathop \in A} f_i^{-1} \sqbrk {\bigcap_{i \mathop = 1}^{n_\alpha} U_{\alpha, n_\alpha} }
		| c = Preimage of Union under Mapping
}}
{{eqn	| r = \bigcup_{\alpha \mathop \in A} \, \bigcap_{i \mathop = 1}^{n_\alpha} f_i^{-1} \sqbrk {U_{\alpha, n_\alpha} }
		| c = Preimage of Intersection under Mapping
}}
{{end-eqn}}
where $f_i^{-1} \sqbrk {U_{\alpha, n_\alpha} } \in \SS$ for each $\alpha \in A$. 
So $f_i^{-1} \sqbrk U$ can be expressed as the set union of finite intersections of elements of $\map \tau \SS$.
Since topologies are closed under unions and finite intersections, for each $i \in I$ and $U \in \tau_i$ we have $f_i^{-1} \sqbrk U \in \map \tau \SS$. 
So we have shown that: 
:$\SS' \subseteq \map \tau \SS$
so that: 
:$\tau = \map \tau {\SS'} \subseteq \map \tau {\SS'}$ 
giving:
:$\map \tau \SS = \map \tau {\SS'} = \tau$
So $\SS$ is a synthetic sub-basis for $\struct {X, \tau}$.
{{qed}}
Category:Initial Topology
Category:Topological Bases
2as16fnwmfm0ql07zc18f3gfv3ip8y4