nyuuzyou/wikis huggingface dataset:
Existence of Middle Universal Product

== Theorem ==
For each $m \in \N$, the following is a theorem of von Neumann-Bernays-Gödel set theory:
:$\forall X: \exists Z: \forall v_1, \dotsc, v_m: \forall x, y: \sequence {x, v_1, \dotsc, v_m, y} \in Z \iff \tuple {x, y} \in X$
where the notation $\sequence {\cdot, \dotsc, \cdot}$ is defined inductively as:
:$\sequence {y_1} := y_1$
:$\sequence {y_1, \dotsc, y_k, y_{k + 1}} := \tuple {\sequence {y_1, \dotsc, y_k}, y_{k + 1}}$
and $\tuple {\cdot, \cdot}$ denotes the Kuratowski formalization of ordered pairs.
=== Corollary ===
== Proof ==
In the metatheory in which NBG is formalized, we proceed by induction on $m$.
=== Basis for the Induction ===
If $m = 0$, the theorem is:
:$\forall X: \exists Z: \forall x, y: \sequence {x, y} \in Z \iff \tuple {x, y} \in X$
But, by unfolding the definition of $\sequence {x, y}$, we observe that it is precisely $\tuple {x, y}$.
Therefore, $Z := X$ satisfies the basis for the induction.
=== Induction Hypothesis ===
As the induction hypothesis, assume that:
:$\forall X: \exists Z: \forall v_1, \dotsc, v_m: \forall x, y: \sequence {x, v_1, \dotsc, v_m, y} \in Z \iff \tuple {x, y} \in X$
for some arbitrary $m \in \N$
From this, we will prove:
:$\forall X: \exists Z: \forall v_1, \dotsc, v_m, v_{m + 1}: \forall x, y: \sequence {x, v_1, \dotsc, v_m, v_{m + 1}, y} \in Z \iff \tuple {x, y} \in X$
=== Induction Step ===
Let $X$ be arbitrary.
Apply the induction hypothesis to find a class $Z$ such that:
:$\forall v_1, \dotsc, v_m: \forall x, y: \sequence {x, v_1, \dotsc, v_m, y} \in Z \iff \tuple {x, y} \in X$
Next we will use the following:
==== Lemma ====
Applying the lemma to $Z$, there is a class $Z'$ such that:
:$\forall u, v, w: \tuple {\tuple {u, v}, w} \in Z' \iff \tuple {u, w} \in Z$
In particular, for $u = \sequence {x, v_1, \dotsc, v_m}$, $v = v_{m + 1}$, and $w = y$:
:$\forall v_1, \dotsc, v_m: \forall x, y: \tuple {\tuple {\sequence {x, v_1, \dotsc, v_m}, v_{m + 1}}, y} \in Z' \iff \tuple {\sequence {x, v_1, \dotsc, v_m}, y} \in Z$
But by definition of the notation $\sequence {\cdot, \dotsc, \cdot}$, that is equivalent to:
:$\forall v_1, \dotsc, v_m: \forall x, y: \sequence {x, v_1, \dotsc, v_m, v_{m + 1}, y} \in Z' \iff \sequence {x, v_1, \dotsc, v_m, y} \in Z$
Finally, by Biconditional is Transitive with the definition of $Z$:
:$\forall v_1, \dotsc, v_m: \forall x, y: \sequence {x, v_1, \dotsc, v_m, v_{m + 1}, y} \in Z' \iff \tuple {x, y} \in X$
Therefore, $Z'$ satisfies the induction step.
By the Principle of Mathematical Induction, the theorem follows.
Category:Class Theory
Category:Von Neumann-Bernays-Gödel Set Theory
Existence of Middle Universal Product/Corollary

== Corollary to Existence of Middle Universal Product ==
For each $n \in \N_{> 0}$ and $m \in \N$, the following is a theorem of von Neumann-Bernays-Gödel set theory:
:$\forall X: \exists Z: \forall v_1, \dotsc, v_m: \forall x_1, \dotsc, x_n: \forall y: \sequence {x_1, \dotsc, x_n, v_1, \dotsc, v_m, y} \in Z \iff \sequence {x_1, \dotsc, x_n, y} \in X$
where the notation $\sequence {\cdot, \dotsc, \cdot}$ is defined inductively as:
:$\sequence {y_1} := y_1$
:$\sequence {y_1, \dotsc, y_k, y_{k + 1}} := \tuple {\sequence {y_1, \dotsc, y_k}, y_{k + 1}}$
and $\tuple {\cdot, \cdot}$ denotes the Kuratowski formalization of ordered pairs.
== Proof ==
Let $X$ be arbitrary.
By Existence of Middle Universal Product, there is a class $Z$ such that:
:$\forall v_1, \dotsc, v_m: \forall x, y: \sequence {x, v_1, \dotsc, v_m, y} \in Z \iff \tuple {x, y} \in X$
In particular, for $x = \sequence {x_1, \dotsc, x_n}$:
:$\forall v_1, \dotsc, v_m: \forall x_1, \dotsc, x_n: \forall y: \sequence {\sequence {x_1, \dotsc, x_n}, v_1, \dotsc, v_m, y} \in Z \iff \tuple {\sequence {x_1, \dotsc, x_n}, y} \in X$
But, by the definition of the notation $\sequence {\cdot, \dotsc, \cdot}$, this is equivalent to:
:$\forall v_1, \dotsc, v_m: \forall x_1, \dotsc, x_n: \forall y: \sequence {x_1, \dotsc, x_n, v_1, \dotsc, v_m, y} \in Z \iff \sequence {x_1, \dotsc, x_n, y} \in X$
Thus, the theorem holds.
Existence of Middle Universal Product/Lemma

== Lemma for Existence of Middle Universal Product ==
The following is a theorem of von Neumann-Bernays-Gödel set theory:
:$\forall X: \exists Z: \forall u, v, w: \tuple {\tuple {u, v}, w} \in Z \iff \tuple {u, w} \in X$
== Proof ==
Let $X$ be arbitrary.
By Axiom $\text B 5$, there exists some class $Z$ such that:
:$\forall x, v: \tuple {x, v} \in Z \iff x \in X$
In particular, for $x = \tuple {u, w}$:
:$\forall u, v, w: \tuple {\tuple {u, w}, v} \in Z \iff \tuple {u, w} \in X$
Now, by Axiom $\text B 7$, there is a class $Z'$ such that:
:$\forall u, v, w: \tuple {\tuple {u, v}, w} \in Z' \iff \tuple {\tuple {u, w}, v} \in Z$
Thus, by Biconditional is Transitive:
:$\forall u, v, w: \tuple {\tuple {u, v}, w} \in Z' \iff \tuple {u, w} \in X$
which satisfies the theorem.
Existence of Minimal Hausdorff Space which is not Compact

== Theorem ==
Let $S$ be a set.
Let $\tau$ be the minimal subset of the power set $\powerset S$ such that $\struct {S, \tau}$ is a Hausdorff space.
Then it is not necessarily the case that $\struct {S, \tau}$ is compact.
== Proof ==
Let $T = \struct {S, \tau}$ be the canonical minimal Hausdorff non-compact space.
This space has been so named on in order to allow reference to it without needing to describe it whenever it is mentioned.
By Canonical Minimal Hausdorff Non-Compact Space is Minimal Hausdorff, $\tau$ is the minimal subset of the power set $\powerset S$ such that $T$ is a Hausdorff space.
By Canonical Minimal Hausdorff Non-Compact Space is not Compact, $T$ is not a compact topological space.
Hence the result.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $3$: Compactness: Compactness Properties and the $T_i$ Axioms
Category:Hausdorff Spaces
Category:Compact Spaces
Existence of Minimal Polynomial for Square Matrix over Field

== Theorem ==
Let $K$ be a field.
Let $n$ be a natural number.
Let $K^{n \times n}$ be the set of $n \times n$ matrices over $K$. 
Let $A \in K^{n \times n}$.
Then the minimal polynomial of $A$ exists and has degree at most $n^2$.
== Proof ==
By Matrices over Field form Vector Space:
:$K^{n \times n}$ forms a vector space under usual matrix addition and scalar multiplication.
By Dimension of Vector Space of Matrices:
:$K^{n \times n}$ has dimension $n^2$. 
Consider the collection of vectors: 
:$I, A, A^2, \ldots, A^{n^2}$
Since this is a collection of $n^2 + 1$ vectors, and $K^{n \times n}$ has dimension $n^2$, we have by Size of Linearly Independent Subset is at Most Size of Finite Generator:
:$I, A, A^2, \ldots, A^{n^2}$ are linearly dependent.
That is, there exists $\alpha_0, \alpha_1, \ldots, \alpha_{n^2} \in K$ not all zero such that: 
:$\ds \sum_{i \mathop = 0}^{n^2} \alpha_i A^i = 0$
That is, the polynomial: 
:$\ds \sum_{i \mathop = 0}^{n^2} \alpha_i X^i \in K \sqbrk X$
has $\map P A = 0$, and degree at most $n^2$. 
Let: 
:$S = \set {P \in K \sqbrk X \setminus \set 0 \mid \map P A = 0}$ 
$S$ is certainly non-empty since we have found such an element in the computation above. 
Now consider the set: 
:$D = \set {\deg P \mid P \in S}$
Since $D$ is a subset of the natural numbers, it contains a least element $N$ by the Well-Ordering Principle.
Since the polynomial we constructed has degree at most $n^2$, we have $N \le n^2$.
Let $Q \in S$ be of degree $N$.
Let $a_N$ be the coefficient of the $X^N$ term in $Q$. 
Then $\mu = \dfrac 1 {a_N} Q$ is a monic polynomial of minimum degree with $\map \mu A = 0$. 
So $\mu$ is a minimal polynomial for $A$. 
Category:Linear Algebra
Category:Minimal Polynomials
Existence of Minimal Uncountable Well-Ordered Set

== Theorem ==
There exists a minimal uncountable well-ordered set.
That is, there exists an uncountable well-ordered set $\Omega$ with the property that every initial segment in $\Omega$ is countable.
=== Corollary 1 ===
=== Corollary 2 ===
== Proof Using Choice ==
== Proof Without Using Choice ==
== Also see ==
* Minimal Uncountable Well-Ordered Set Unique up to Isomorphism
Category:Order Theory
Category:Existence of Minimal Uncountable Well-Ordered Set
Existence of Minimal Uncountable Well-Ordered Set/Corollary 1

== Corollary to Existence of Minimal Uncountable Well-Ordered Set ==
Let $\Omega$ denote the minimal uncountable well-ordered set.
The cardinality of $\Omega$ satisfies:
:$\card \N < \card \Omega \le \mathfrak c$
where $\card \N$ is the cardinality of the natural numbers and $\mathfrak c$ is the cardinality of the continuum.
== Proof ==
By the definition of $\Omega$ as a minimal uncountable well-ordered set:
:$\card \N < \card \Omega$
by the definition of uncountable.
Furthermore:
:$\card \Omega \le \card {\powerset \N}$ follows the from construction of $\Omega$ in the main proofs; $\Omega$ is a subset of $\powerset \N$.
That $\card {\powerset \N} = \mathfrak c$ is shown in Power Set of Natural Numbers has Cardinality of Continuum.
Combining the above statements yields:
:$\card \N < \card \Omega \le \mathfrak c$
== Sources == 
* $\S P.18$ 
* $\S 1.11$ Supplementary Exercise $8$
Category:Existence of Minimal Uncountable Well-Ordered Set
Existence of Minimal Uncountable Well-Ordered Set/Corollary 2

== Corollary to Existence of Minimal Uncountable Well-Ordered Set ==
Let $X$ be a well-ordered set.
Then there exists a well-ordered set with cardinality strictly greater than $X$.
== Proof ==
Follows from the same arguments proving the main result, , replacing:
:"$\powerset \N$" with "$\powerset X$"
:"Power Set of Natural Numbers is not Countable" with "No Bijection from Set to its Power Set"
:"is uncountable" with "has cardinality $\size {\powerset X}$"
:"is countable" with "has cardinality strictly less than $\size {\powerset X}$"
== Sources == 
* $\S 1.11$ Supplementary Exercise $8$
Category:Existence of Minimal Uncountable Well-Ordered Set
Existence of Minimal Uncountable Well-Ordered Set/Proof Using Choice

== Theorem ==
== Proof ==
By the axiom of powers, there exists the power set $\powerset \N$, where $\N$ is the set of natural numbers.
By Power Set of Natural Numbers is not Countable, this set is uncountable.
By Zermelo's Well-Ordering Theorem, $\powerset \N$ can be endowed with a well-ordering.
Denote such an ordering with the symbol $\preccurlyeq$.
Let $\powerset \N_a$ denote the initial segments of $\powerset \N$ determined by $a \in \powerset \N$ 
Suppose $\struct {\powerset \N, \preccurlyeq}$ has the property:
:$\powerset \N_a$ is countable for every $a \in \powerset \N$
Then set $\Omega = \powerset \N$.
Otherwise, suppose $\struct {\powerset \N, \preccurlyeq}$ does not have the above property.
Consider the subset of $\powerset \N$:
:$P \subseteq \set {a \in \powerset \N : \powerset \N_a \text{ is uncountable} }$
Then $P$ has a smallest element, by the definition of a well-ordered set.
Call such an element $a_0$.
That is, $a_0 \in \powerset \N$ is the smallest $a$ such that $\powerset \N_{a_0}$ is uncountable.
Then the initial segment $\powerset \N_{a_0}$ is itself uncountable, by virtue of $a_0$ being in $P$.
Thus every initial segment in $\powerset \N_{a_0}$ is countable, because it is not uncountable.
Then:
:$\Omega = \powerset \N_{a_0}$
== Sources ==
* $\S \text P.18$
Category:Existence of Minimal Uncountable Well-Ordered Set
Existence of Negation Normal Form of Statement

== Theorem ==
Any propositional formula can be expressed in negation normal form (NNF).
== Proof ==
A propositional variable is already trivially in negation normal form (NNF).
So we consider the general propositional formula $S$.
In the following, $P$ and $Q$ are to stand for general propositional formulas.
First, from Functionally Complete Logical Connectives: Conjunction, Negation and Disjunction we have that:
:$\set {\neg, \land, \lor}$
forms a functionally complete set of logical connectives.
So we can convert $S$ so that:
:by the definition of the biconditional, instances of $P \iff Q$ can be converted into $\paren {P \implies Q} \land \paren {Q \implies P}$
:by the Rule of Material Implication, instances of $P \implies Q$ can be converted into $\neg P \lor Q$.
Other connectives can likewise be treated appropriately.
Thus $S$ will contain nothing but connectives from $\set {\neg, \land, \lor}$.
Next we can replace:
:instances of $\neg \paren {P \land Q}$ with $\neg P \lor \neg Q$, by De Morgan's Laws: Disjunction of Negations
:instances of $\neg \paren {P \lor Q}$ with $\neg P \land \neg Q$, by De Morgan's Laws: Conjunction of Negations
:instances of $\neg \neg P$ with $P$ by Double Negation Elimination.
At any stage where a negation appears before a parenthesis, it will then appear before the statements inside the parenthesis.
Thus the negation signs gradually move inwards or are eliminated.
Eventually all remaining negation signs will appear next to simple statements.
Hence the result.
Category:Propositional Logic
Existence of Niven Number for Any Sum of Digits

== Theorem ==
Let $b, s$ be integers such that $b > 1$ and $s > 0$.
Then there exists a Niven Number in base $b$ with sum of digits $s$.
== Proof ==
Consider the prime factorization of $b$:
:$b = p_1^{a_1} p_2^{a_2} \dots p_k^{a_k}$
where $a_1, a_2, \dots, a_k \ge 1$.
Write:
:$s = p_1^{c_1} p_2^{c_2} \dots p_k^{c_k} t$
where $b$ and $t$ are coprime.
Let $c = \max \set {c_1, c_2, \dots, c_k}$.
We will show that the number:
:$n = b^c \paren {b^{\map \phi t} + b^{2 \map \phi t} + \dots + b^{s \map \phi t} }$
is a Niven Number in base $b$, where $\map \phi t$ denotes the Euler totient function.
Notice that $n$ is a sum of distinct powers of $b$.
By Basis Representation Theorem, we can write:
:$\ds n = \sum_{j \mathop = 0}^d r_j b^j$
and we see that:
:$r_j = 1$ for $j = c + x \map \phi t$ for $x = 1, 2, \dots, s$
:$r_j = 0$ otherwise
Therefore the base $b$ representation of $n$ contains $s$ $1$'s and all other digits are zero.
Thus the sum of digits of $n$ in base $b$ is $s$.
It remains to show that $n$ is divisible by $s$.
We have:
:$c_i \le c \le a_1 c$
for any $1 \le i \le k$.
Thus we have, by Product of Divisors is Divisor of Product:
:$\dfrac s t = p_1^{c_1} p_2^{c_2} \dots p_k^{c_k} \divides p_1^{a_1 c} p_2^{a_2 c} \dots p_k^{a_k c} = b^c$
We also have:
and thus $t \divides b^{\map \phi t} + b^{2 \map \phi t} + \dots + b^{s \map \phi t}$.
By Product of Divisors is Divisor of Product again:
:$s = \dfrac s t \times t \divides b^c \paren {b^{\map \phi t} + b^{2 \map \phi t} + \dots + b^{s \map \phi t} } = n$
Hence the result.
== Sources ==
* : No. $37$
Category:Harshad Numbers
Existence of Non-Empty Finite Infima in Meet Semilattice

== Theorem ==
Let $\struct {S, \preceq}$ be a meet semilattice.
Let $A$ be a non-empty finite subset of $S$.
Then $A$ admits a infimum in $\struct {S, \preceq}$.
== Proof ==
This follows by mutatis mutandis of the proof of Existence of Non-Empty Finite Suprema in Join Semilattice.
== Sources ==
* 
* 
Category:Join and Meet Semilattices
Existence of Non-Empty Finite Suprema in Join Semilattice

== Theorem ==
Let $\struct {S, \preceq}$ be a join semilattice.
Let $A$ be a non-empty finite subset of $S$.
Then $A$ admits a supremum in $\struct {S, \preceq}$.
== Proof ==
We will prove by induction of the cardinality of finite subset of $H$.
=== Base case ===
:$\forall A \subseteq S: \card A = 1 \implies \exists \sup A$
where $\card A$ denotes the cardinality of $A$.
Let $A \subseteq S$ such that
:$\card A = 1$
By Cardinality of Singleton:
:$\exists a: A = \set a$
By definition of subset:
:$a \in S$
Thus by Supremum of Singleton:
:the supremum of $A$ exists in $\struct {S, \preceq}$.
=== Induction Hypothesis ===
:$n \ge 1 \land \forall A \subseteq S: \card A = n \implies \exists \sup A$
=== Induction Step ===
:$\forall A \subseteq S: \card A = n + 1 \implies \exists \sup A$
Let $A \subseteq S$ such that:
:$\card A = n + 1$
By definition of cardinality of finite set:
:$A \sim \N_{< n + 1}$
where $\sim$ denotes set equivalence.
By definition of set equivalence:
:there exists a bijection $f: \N_{< n + 1} \to A$
By Restriction of Injection is Injection:
:$f \restriction_{\N_{< n} }: \N_{< n} \to f^\to \sqbrk {\N_{< n} }$ is an injection.
By definition:
:$f \restriction_{\N_{< n} }: \N_{< n} \to f^\to \sqbrk {\N_{< n} }$ is a surjection.
By definition:
:$f \restriction_{\N_{< n} }: \N_{< n} \to f^\to \sqbrk {\N_{< n} }$ is a bijection.
By definition of set equivalence:
:$\N_{< n} \sim f^\to \sqbrk {\N_{< n} }$
By definition of cardinality of finite set:
:$\card {f^\to \sqbrk {\N_{< n} } } = n$
By definitions of image of set and subset:
:$f^\to \sqbrk {\N_{< n} } \subseteq A$
By Subset Relation is Transitive:
:$f^\to \sqbrk {\N_{< n} } \subseteq S$
By Induction Hypothesis:
:$\exists \map \sup {f^\to \sqbrk {\N_{< n} } }$
By definition $\N_{< n + 1}$:
:$n \in \N_{< n + 1}$
By definition of mapping:
:$\map f n \in A$
By definition of subset:
:$\map f n \in S$
Thus:
Thus $A$ admits a supremum in $\struct {S, \preceq}$.
== Sources ==
* 
* 
Category:Join and Meet Semilattices
Existence of Non-Locally Connected Space where Components and Quasicomponents are Equal

== Theorem ==
There exists at least one example of a topological space which is not locally connected, but whose components and quasicomponents are equal.
== Proof ==
Let $T$ be the Arens-Fort space.
From Arens-Fort Space is not Locally Connected, $T$ is not a locally connected space.
The result follows from Components and Quasicomponents of Arens-Fort Space are Equal.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $4$: Connectedness
Category:Locally Connected Spaces
Category:Components
Category:Quasicomponents
Existence of Non-Square Residue

== Theorem ==
Let $m \in \Z$ be an integer such that $m > 2$.
Let $\Z_m$ be the set of integers modulo $m$:
:$\Z_m = \set {\eqclass 0 m, \eqclass 1 m, \ldots, \eqclass {m - 1} m}$
Then there exists at least one residue in $\Z_m$ which is not the product modulo $m$ of a residue with itself:
:$\exists p \in \Z_m: \forall x \in \Z_m: x \cdot_m x \ne p$
== Proof ==
We have that $1 \in \Z_m$ and that:
:$1 \cdot_m 1 = 1$
We have that $m - 1 \in \Z_m$ and that:
:$\paren {m - 1} \cdot_m \paren {m - 1} = 1$
Thus unless $m - 1 = 1$, that is, $m = 2$, there exist $2$ residues of $\Z_m$ whose product modulo $m$ with itself equals $1$.
There are $m - 2$ residues which, when multiplied modulo $m$ with themselves have as a result a residue.
Thus there can be at maximum $m - 2$ residues (excluding $1$) which can be the product modulo $m$ of a residue with itself.
But there are $m - 1$ residues (excluding $1$).
So at least $1$ residue is not the product modulo $m$ of a residue with itself.
== Sources ==
* : Exercise $2.5$
Category:Modulo Arithmetic
Existence of Non-Standard Models of Arithmetic

== Theorem ==
There exist non-standard models of arithmetic.
== Proof ==
Let $P$ be the set of axioms of Peano arithmetic.
Let $Q = P \cup \left\{{\neg x = 0, \neg x = s0, \neg x = ss0, \ldots}\right\}$ where $x$ is a variable of the language.
Then each finite subset of $Q$ is satisfied by the standard model of arithmetic
Hence $Q$ is satisfiable by the Compactness theorem.
But any model satisfying $Q$ must assign $x$ to an element which cannot be obtained by iterating the successor operator on zero a finite number of times.
Category:Mathematical Logic
Existence of Non-Zero Continuous Linear Functional vanishing on Proper Closed Subspace of Hausdorff Locally Convex Space

== Theorem ==
Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \PP}$ be a Hausdorff locally convex space over $\GF$.
Let $Y$ be a proper closed linear subspace of $X$.
Let $x_0 \in X \setminus Y$. 
Then there exists a continuous linear functional $f : X \to \GF$ such that: 
:$\map f y = 0$ for each $y \in Y$
and:
:$\map f {x_0} \ne 0$
== Proof ==
Let:
:$X_0 = \map \span {Y \cup \set x}$
From Linear Span is Linear Subspace, we have: 
:$X_0$ is a linear subspace of $X$.
Note that we can then write any $u \in X_0$ in the form: 
:$u = y + \alpha x$
for $y \in Y$ and $\alpha \in \mathbb F$. 
We want to define a map in terms of this representation, so we show that this representation is unique. 
Let: 
:$u = y_1 + \alpha_1 x = y_2 + \alpha_2 x$
Then: 
:$\paren {\alpha_2 - \alpha_1} x = y_1 - y_2$
If $\alpha_1 = \alpha_2$, then we have $y_1 = y_2$ as required.
 suppose that $\alpha_1 \ne \alpha_2$, then we would have: 
:$\ds x = \frac 1 {\alpha_2 - \alpha_1} \paren {y_1 - y_2}$
and so $x \in Y$, from the definition of a linear subspace, contradiction. 
So, we must have $\alpha_1 = \alpha_2$ and $y_1 = y_2$, and so the representation is unique. 
Now, define $f_0 : X_0 \to \GF$ by: 
:$\map {f_0} {y + \lambda x_0} = \lambda$
for each $y \in Y$, $\lambda \in \GF$.
We have $\map {f_0} x = 0$ $x \in Y$, so that: 
:$\ker f_0 = Y$
This is closed, so by Characterization of Continuous Linear Functionals on Topological Vector Space, we have: 
:$f_0$ is continuous. 
From Hahn-Banach Theorem for Continuous Linear Functional on Locally Convex Space, there exists a continuous linear functional $f$ extending $f_0$. 
Then we have: 
:$\map f {x_0} = \map {f_0} {x_0} = 1 \ne 0$ 
and: 
:$\map f y = \map {f_0} y = 0$
for each $y \in Y$.
So $f$ is a continuous linear functional satisfying our requirements.
Category:Linear Functionals
Category:Locally Convex Spaces
Existence of Nonconstant Periodic Function with no Period

== Theorem ==
There exists a real, non-constant function $f$ such that:
:$(1): \quad f$ is periodic.
:$(2): \quad f$ does not have a period.
== Proof ==
By Dirichlet Function is Periodic and Dirichlet Function has no Period, it is seen that the Dirichlet functions are such an example.
Category:Periodic Functions
Existence of Nonprincipal Ultrafilter

== Theorem ==
Let $S$ be an infinite set.
Then there exists an nonprincipal ultrafilter $U$ on $S$.
== Proof ==
Let $\FF$ be the Fréchet filter on $S$.
By Fréchet Filter is Filter, $\FF$ is a filter on $S$.
Then, by the Ultrafilter Lemma, there exists some ultrafilter $U \supseteq \FF$ on $S$.
Let $a \in S$ be arbitrary.
By Existence of Singleton Set, there exists a singleton $\set a$.
Let $A = S \setminus \set a$.
By the definition of set difference, $a \notin A$.
Then:
But by Singleton is Finite, $\set a$ is a finite set.
Therefore, $S \setminus A$ is finite as well.
But then, by definition, $A$ is cofinite in $S$.
Thus, by definition of Fréchet filter, $A \in \FF$.
But as $U \supseteq \FF$, $A \in U$ by definition of superset.
Therefore, as $a \in S$ was arbitrary:
:For every $a \in S$, there is some $A \in U$ such that $a \notin A$.
Thus, $U$ does not have a cluster point, and is nonprincipal by definition.
Category:Filter Theory
Existence of Normal Bundle to Pseudo-Riemannian Submanifold

== Theorem ==
Let $\struct {\tilde M, \tilde g}$ be a pseudo-Riemannian manifold.
Let $M \subseteq \tilde M$ be an embedded pseudo-Riemannian or Riemannian submanifold. 
Let $NM$ be the normal bundle of $M$.
Then $NM$ is a smooth vector subbundle of $\valueat {T \tilde M} M$.
== Proof ==
== Sources ==
* : $\S 2$: Riemannian Metrics. Pseudo-Riemannian Metrics
Category:Pseudo-Riemannian Geometry
Existence of Normal Space which is not Completely Normal

== Theorem ==
There exists at least one example of a topological space which is a normal space, but is not also a completely normal space.
== Proof ==
Let $T$ be a Tychonoff plank.
From Tychonoff Plank is Normal, $T$ is a normal space.
From Tychonoff Plank is not Completely Normal, $T$ is not a completely normal space.
Hence the result.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $2$: Separation Axioms: Completely Regular Spaces
Category:Separation Axioms
Category:Normal Spaces
Category:Completely Normal Spaces
Existence of Number to Power of Prime Minus 1 less 1 divisible by Prime Squared

== Theorem ==
Let $p$ be a prime number.
Then there exists at least one positive integer $n$ greater than $1$ such that:
:$n^{p - 1} \equiv 1 \pmod {p^2}$
== Proof ==
Hence $p^2 + 1$ fulfils the conditions for the value of $n$ whose existence was required to be demonstrated.
== Examples ==
== Sources ==
* : $64$
* : $64$
Category:Number Theory
Category:Existence of Number to Power of Prime Minus 1 less 1 divisible by Prime Squared