nyuuzyou/wikis huggingface dataset:
Normed Vector Space is Separable iff Weakly Separable

== Theorem ==
Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \norm {\, \cdot \,} }$ be a normed vector space over $\GF$.
Let $w$ be the weak topology on $X$.
Then $\struct {X, \norm {\, \cdot \,} }$ is separable $\struct {X, w}$ is separable. 
== Proof ==
=== Necessary Condition ===
This follows from Separable Topological Space remains Separable in Coarser Topology.
=== Sufficient Conditon ===
Suppose that $\struct {X, w}$ is separable.
Let $D$ be a countable dense subset of $\struct {X, w}$.
From Set Closure Preserves Set Inclusion, we have: 
:$\map {\cl_w} D \subseteq \map {\cl_w} {\map \span D}$
So that: 
:$\map {\cl_w} {\map \span D} = X$
From Mazur's Theorem, we then have: 
:$\map \cl {\map \span D} = X$
From Closed Linear Span of Countable Set in Topological Vector Space is Separable, we have: 
:$\struct {\map \cl {\map \span D}, \norm {\, \cdot \,} }$ is separable.
So $\struct {X, \norm {\, \cdot \,} }$ is separable.
== Sources ==
* : Proposition $3.26$
Category:Weak Topologies on Topological Vector Spaces
Category:Separable Spaces
Normed Vector Space of Bounded Sequences is not Separable

== Theorem ==
Let $\struct {\ell^\infty, \norm {\, \cdot \,}_\infty}$ be the normed vector space of bounded sequences.
$\struct {\ell^\infty, \norm {\, \cdot \,}_\infty}$ is not separable.
== Proof ==
 $\struct {\ell^\infty, \norm {\, \cdot \,}_\infty}$ is separable.
Let $\mathbf x := \sequence {x_i}_{i \mathop \in \N}$, $\mathbf a := \sequence {a_i}_{i \mathop \in \N}$, $\mathbf b := \sequence {b_i}_{i \mathop \in \N}$ be sequences.
Let $D := \set {\mathbf x_i \in \R^\N : i \in \N}$ be a dense countable subset of $\ell^\infty$.
Let $A := \set {\sequence {y_i}_{i \mathop \in \N} : y_i = 0 \text{ or } y_i = 1}$ be the set of all sequences with terms equal to either $0$ or $1$.
Suppose $\mathbf a, \mathbf b \in A$ are two distinct elements of $A$.
Then:
:$\exists n \in \N : a_n \ne b_n$
and:
Hence, their mutual distance is $1$.
Since $D$ is dense in $\ell^\infty$, we have that:
:$\ds \forall \mathbf a \in A : \exists \mathbf x_{\map i {\mathbf a} } \in \map {B_{\frac 1 3} } {\mathbf a}$
For all $\mathbf a \in A$, the open balls $\map {B_{\frac 1 3} } {\mathbf a}$ are mutually disjoint because $\ds \frac 1 3 + \frac 1 3 < 1$.
Hence:
:$\forall {\mathbf a} \in A : \forall n \in \N : \mathbf a \mapsto \map n {\mathbf a}$
is an injection.
By definition, $A$ is countable.
However, $A$ is in a one-to-one correspondence with all real numbers via binary expansion.
Therefore, $A$ is uncountable.
Hence the contradiction.
== Sources ==
* : Chapter $\S 1.3$: Normed and Banach spaces. Topology of normed spaces
Category:Separable Spaces
Normed Vector Space of Rational Numbers is not Banach Space

== Theorem ==
Let $\struct {\Q, \size {\, \cdot \,}}$ be the normed vector space of rational numbers.
Then $\struct {\Q, \size {\, \cdot \,}}$ is not a Banach space.
== Proof ==
Let $\sequence {x_n}_{n \mathop \in \N}$ be a sequence in $\Q$ defined recursively in the following way:
:$\ds x_0 = \frac 3 2$
:$\ds \forall n \in \N_{> 0} : x_{n \mathop + 1} = \frac {4 + 3 x_n} {3 + 2 x_n}$
We have that:
:$\forall n \in \N : x_n \ge 0$
Note that:
Hence:
:$\paren {x_n \ge \sqrt 2} \implies \paren {x_{n \mathop + 1} \ge \sqrt 2}$
For $n = 0$ we have $\ds \frac 9 4 \ge 2$, or $\ds \frac 3 2 \ge \sqrt 2$.
Therefore:
:$\forall n \in \N : x_n \ge \sqrt 2$
Furthermore:
Hence:
:$\forall n \in \N : x_n \ge x_{n \mathop + 1}$
By monotone convergence theorem, $\sequence {x_n}_{n \mathop \in \N}$ converges in $\struct {\R, \size {\, \cdot \,}}$.
By Convergent Sequence in Normed Vector Space is Cauchy Sequence, $\sequence {x_n}_{n \mathop \in \N}$ is Cauchy in $\struct {\R, \size {\, \cdot \,}}$.
On the other hand:
:$\forall n \in \N : x_n \in \Q$
Thus, $\sequence {x_n}_{n \mathop \in \N}$ is also Cauchy in $\struct {\Q, \size {\, \cdot \,}}$.
Suppose $\sequence {x_n}_{n \mathop \in \N}$ converges to $L \in \Q$.
By combination theorem for sequences:
:$\ds L = \frac {4 + 3 L} {3 + 2 L}$
or $L^2 = 2$.
$L$ has to be positive, so $L = \sqrt 2$.
However, $\sqrt 2 \notin \Q$.
Hence, $\sequence {x_n}_{n \mathop \in \N}$ does not converge in $\struct {\Q, \size {\, \cdot \,} }$.
Altogether, we have that $\sequence {x_n}_{n \mathop \in \N} \in \Q$ is a Cauchy sequence which is not convergent in $\struct {\Q, \size {\, \cdot \,} }$.
By definition, $\struct {\Q, \size {\, \cdot \,}}$ is not a Banach space.
== Also see ==
* Rational Number Space is not Complete Metric Space
== Sources ==
* : $\S 1.4$: Normed and Banach spaces. Sequences in a normed space; Banach spaces
Category:Rational Number Space
Normed Vector Space over Complex Numbers with Schauder Basis is Separable

== Theorem ==
Let $\struct {X, \norm {\, \cdot \,}}$ be a normed vector space over $\C$.
Suppose $X$ admits a Schauder basis.
Then $X$ is separable.
== Proof ==
Let $\set {\mathbf E_i : i \in \N}$ be a Schauder basis.
Then:
:$\ds \forall x \in X : \exists \sequence {x_i'}_{i \mathop \in \N} \in \C : x = \sum_{i \mathop = 0}^\infty x_i' \mathbf E_i$
Let $\ds \mathbf e_i = \frac {\mathbf E_i}{\norm {\mathbf E_i}}$ and $\ds x_i=x_i' \norm{\mathbf E_i}$.
Then $\ds x = \sum_{i \mathop = 0}^\infty x_i \mathbf e_i$ where $\forall i \in \N : \norm {\mathbf e_i} = 1$.
Let $\ds Y = \set {\sum_{i \mathop = 0}^n q_i \mathbf e_i : q_i \in \Q \sqbrk i, n \in \N}$ be a countable set.
$Y$ is spanned by $\set {\mathbf e_i : i \in \N}$.
Also, Gaussian Rational Numbers form Subset of Complex Numbers.
Hence, $Y \subseteq X$.
We have that Gaussian Rationals are Everywhere Dense in Complex Numbers.
Then for any $i \in \N$:
:$\forall x_i \in \C: \forall \epsilon_i \in \R_{>0}: \exists q_i \in \Q \sqbrk i: \size {x_i - q_i} < \epsilon_i$
Hence:
By the existence of Schauder basis, the limit $\ds x = \sum_{i \mathop = 0}^\infty x_i \mathbf e_i$ exists.
Thus:
:$\ds \forall \epsilon' \in \R_{>0}: \exists N \in \R_{>0}: \forall n \in \N: n > N \implies \norm {\sum_{i \mathop = 0}^\infty x_i \mathbf e_i - \sum_{i \mathop = 0}^n x_i \mathbf e_i} < \epsilon'$
Therefore:
Let $\epsilon \in \R_{> 0}$. 
Let $\epsilon'$ and $\sequence {\epsilon_i}_{0 \mathop \le i \le n}$ be such that:
:$\ds \epsilon > \epsilon' + \sum_{i \mathop = 0}^n \epsilon_i$.
Let $n > N$.
Then:
:$\ds \norm {x - \sum_{i \mathop = 0}^n q_i \mathbf e_i} < \epsilon$
$\epsilon$ was arbitrary.
Altogether:
:$\ds \forall x \in X : \forall \epsilon \in \R_{> 0} : \exists y_{i \mathop \in \N} \in Y : \norm {x - y_i} < \epsilon$
By definition, $X$ is separable.
Category:Schauder Bases
Category:Normed Vector Spaces
Category:Separable Spaces
Normed Vector Space with Schauder Basis is Separable

== Theorem ==
Let $\struct {X, \norm {\, \cdot \,}}$ be a normed vector space over $\R$.
Suppose $X$ admits a Schauder basis.
Then $X$ is separable.
== Proof ==
Let $\set {\mathbf E_i : i \in \N}$ be a Schauder basis.
Then:
:$\ds \forall x \in X : \exists \sequence {x_i'}_{i \mathop \in \N} \in \R : x = \sum_{i \mathop = 0}^\infty x_i' \mathbf E_i$
Let $\ds \mathbf e_i = \frac {\mathbf E_i}{\norm {\mathbf E_i}}$ and $\ds x_i=x_i' \norm{\mathbf E_i}$.
Then $\ds x = \sum_{i \mathop = 0}^\infty x_i \mathbf e_i$ where $\forall i \in \N : \norm {\mathbf e_i} = 1$.
Let $\ds Y = \set {\sum_{i \mathop = 0}^n q_i \mathbf e_i : q_i \in \Q, n \in \N}$ be a countable set.
$Y$ is spanned by $\set {\mathbf e_i : i \in \N}$.
Also, Rational Numbers form Subset of Real Numbers.
Hence, $Y \subseteq X$.
We have that rationals are everywhere dense in reals.
Then for any $i \in \N$:
:$\forall x_i \in \R: \forall \epsilon_i \in \R_{>0}: \exists q_i \in \Q: \size {x_i - q_i} < \epsilon_i$
Hence:
By the existence of Schauder basis, the limit $\ds x = \sum_{i \mathop = 0}^\infty x_i \mathbf e_i$ exists.
Thus:
:$\ds \forall \epsilon' \in \R_{>0}: \exists N \in \R_{>0}: \forall n \in \N: n > N \implies \norm {\sum_{i \mathop = 0}^\infty x_i \mathbf e_i - \sum_{i \mathop = 0}^n x_i \mathbf e_i} < \epsilon'$
Therefore:
Let $\epsilon \in \R_{> 0}$. 
Let $\epsilon'$ and $\sequence {\epsilon_i}_{0 \mathop \le i \le n}$ be such that:
:$\ds \epsilon > \epsilon' + \sum_{i \mathop = 0}^n \epsilon_i$.
Let $n > N$.
Then:
:$\ds \norm {x - \sum_{i \mathop = 0}^n q_i \mathbf e_i} < \epsilon$
$\epsilon$ was arbitrary.
Altogether:
:$\ds \forall x \in X : \forall \epsilon \in \R_{> 0} : \exists y_{i \mathop \in \N} \in Y : \norm {x - y_i} < \epsilon$
By definition, $X$ is separable.
== Sources ==
* : Chapter $\S 2.3$: The normed space $\map {CL} {X,Y}$. Operator norm and the normed space $\map {CL} {X, Y}$
Category:Schauder Bases
Category:Normed Vector Spaces
Category:Separable Spaces
Norms Equivalent to Absolute Value on Rational Numbers

== Theorem ==
Let $\alpha \in \R_{> 0}$.
Let $\norm {\,\cdot\,}:\Q \to \R$ be the mapping defined by:
:$\forall x \in \Q: \norm x = \size x^\alpha$
where $\size x$ is the absolute value of $x$ in $\Q$.
Then:
:$\norm {\,\cdot\,}$ be a norm on $\Q$
:
:$\alpha \le 1$
== Proof ==
=== Necessary Condition ===
=== Sufficient Condition ===
== Sources ==
* : $\S 1.2$ Normed fields: Proposition $1.11$ 
Category:Normed Division Rings
Norms Equivalent to Absolute Value on Rational Numbers/Necessary Condition

== Theorem ==
Let $\alpha \in \R_{> 0}$.
Let $\norm {\,\cdot\,}:\Q \to \R$ be the mapping defined by:
:$\forall x \in \Q: \norm x = \size x^\alpha$
where $\size x$ is the absolute value of $x$ in $\Q$.
Let $\norm {\,\cdot\,}$ be a norm on $\Q$.
Then:
:$\alpha \le 1$
== Proof ==
The contrapositive is proved.
Let $\alpha > 1$.
The is not satisfied:
By Rule of Transposition the result follows.
== Sources ==
* : $\S 1.2$ Normed fields, Proposition $1.11$ 
Category:Normed Division Rings
Norms Equivalent to Absolute Value on Rational Numbers/Sufficient Condition

== Theorem ==
Let $\alpha \in \R_{> 0}$.
Let $\norm {\,\cdot\,}: \Q \to \R$ be the mapping defined by:
:$\forall x \in \Q: \norm x = \size x^\alpha$
where $\size x$ is the absolute value of $x$ in $\Q$.
Then:
:$\alpha \le 1 \implies \norm {\,\cdot\,}$ is a norm on $\Q$
== Proof ==
Suppose $\alpha \le 1$.
It is shown that $\norm {\,\cdot\,}$ satisfies the norm axioms $(\text N 1)$-$(\text N 3)$.
=== ===
Let $x \in \Q$.
=== ===
Let $x, y \in \Q$.
Then:
=== ===
Let $x, y \in \Q$.
, let $\norm y < \norm x$.
If $\norm x = 0$ then $\norm y = 0$.
By above:
:$x = y = 0$
Hence:
If $\norm x > 0$ then:
:$\norm x > 0 \leadstoandfrom \size x^\alpha > 0 \leadstoandfrom \size x > 0$
Hence:
== Sources ==
* : $\S 1.2$ Normed fields, Proposition $1.11$ 
Category:Normed Division Rings
Norms of Double Centralizer of C*-Algebra

== Theorem ==
Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $\tuple {L, R}$ be a double centralizer of $A$.
Then $\norm L_{\map B A} = \norm R_{\map B A}$, where $\norm L_{\map B A}$ and $\norm R_{\map B A}$ denotes the norm of a bounded linear transformation.
== Proof ==
For each $a, b \in A$, we have:
Hence by Norm of Element of C*-Algebra as Supremum over Closed Unit Ball, we have:
:$\ds \norm {\map L b} = \sup_{\norm a \le 1} \norm {a \map L b} \le \norm R_{\map B A} \norm b$ 
By the definition of the norm of a bounded linear transformation, we have:
:$\norm L_{\map B A} \le \norm R_{\map B A}$
For each $a, b \in A$, we also have:
Hence by Norm of Element of C*-Algebra as Supremum over Closed Unit Ball, we have:
:$\ds \norm {\map R a} = \sup_{\norm a \le 1} \norm {\map R a b} \le \norm L_{\map B A} \norm b$ 
By the definition of the norm of a bounded linear transformation, we have:
:$\norm R_{\map B A} \le \norm L_{\map B A}$
We conclude:
:$\norm L_{\map B A} = \norm R_{\map B A}$
== Sources ==
* : $2.1$: $\text C^\ast$-Algebras
Category:Multiplier Algebras
Norms on Finite-Dimensional Real Vector Space are Equivalent

== Theorem ==
Norms on finite-dimensional real vector space are equivalent.
== Proof ==
We will prove that all norms are equivalent to $\norm {\, \cdot \,}_2$.
By definition, two norms are equivalent on $\R^d$ :
:$ \exists m, M \in \R_{> 0} : \forall \mathbf x \in \R^d : m \norm {\mathbf x}_a \le \norm {\mathbf x}_b \le M \norm {\mathbf x}_a$
=== "Less or equal" condition ===
Let $\set {\mathbf e_1 \dots \mathbf e_n}$ be a standard basis in $\R^d$.
We have that each $\mathbf x \in \R^d$ is uniquely expressible as:
:$\ds \mathbf x = \sum_{i \mathop = 1}^d x_i \mathbf e_i$
where $x_i$ is a scalar.
Then:
By definition of norm, its image is the set of non-negative real numbers: $M \in \R_{\ge 0}$.
But $M$ is independent of $\mathbf x$.
Hence:
:$\exists M \in \R_{\ge 0} : \forall \mathbf x \in \R^d : \norm {\mathbf x} \le M \norm {\mathbf x}_2$
=== Existence of $m$ ===
Let $K := \set {\mathbf y \in \R^d : \norm {\mathbf y}_2 = 1}$ be a unit sphere in $\struct {\R^d, \norm {\, \cdot \,}_2}$.
By Unit Sphere is Closed in Normed Vector Space, $K$ is closed in $\struct {\R^d, \norm{\, \cdot \,}_2}$.
By definition, $K$ is bounded in $\struct {\R^d, \norm{\, \cdot \,}_2}$.
Hence, by the Heine-Borel theorem, $K$ is a compact set.
By Norm on Vector Space is Continuous Function, the map $\norm {\, \cdot \,} : K \to \R_{\ge 0}$ is continuous from $\struct {K, \norm {\, \cdot \,}_2}$ to $\struct {\R_{\ge 0}, \size {\, \cdot \,}}$:
:$\forall \mathbf y_1, \mathbf y_2 \in K : \size {\norm {\mathbf y_1} - \norm {\mathbf y_2}} \le \norm {\mathbf y_1 - \mathbf y_2} \le M \norm {\mathbf y_1 - \mathbf y_2}_2$
By the Extreme Value Theorem, $\norm {\, \cdot \,} : K \to \R_{\ge 0}$ attains a minimum value $m$ for some $\mathbf y \in K$.
Suppose $m = 0$.
Then:
Furthermore:
:$\forall \mathbf y \in \R^d : \norm {\mathbf y}_2 = 1 : \norm {\mathbf y} \ge m$
=== "Greater or equal" condition ===
Suppose $\mathbf x = 0$.
Then we have equality.
Suppose $\mathbf x \ne 0$.
Let $\ds \mathbf y = \frac {\mathbf x} {\norm {\mathbf x}_2}$.
We have that $\norm {\mathbf y}_2 = 1$ and $\mathbf y \in K$.
Then:
This implies that:
:$m \norm {\mathbf x}_2 \le \norm {\mathbf x}$
But once again, $m$ is independent of $\mathbf x$.
Therefore:
:$\exists m, M : \forall \mathbf x \in \R^d : m \norm {\mathbf x}_2 \le \norm {\mathbf x} \le M \norm {\mathbf x}_2$
By definition, all norms are equivalent to $\norm{\, \cdot \,}_2$.
By Norm Equivalence is Equivalence, the equivalence relation $\norm {\, \cdot \,} \sim \norm {\, \cdot \,}_2$ is transitive.
Thus, all norms are equivalent.
== Sources ==
* : $\S 1.4$: Normed and Banach spaces. Sequences in a normed space; Banach spaces
Category:Normed Vector Spaces
Category:Equivalence Relations
Category:Norm Theory
Category:Vector Spaces
Category:Finite Dimensional Vector Spaces
Not All Natural Number Functions are Primitive Recursive

== Theorem ==
Not all functions $f: \N \to \N$ are primitive recursive.
== Proof ==
All primitive recursive functions are URM computable.
The set of $\mathbf U$ of URM programs is countably infinite.
The set of $\Bbb F$ of natural number functions is uncountably infinite.
Hence there is no surjection from $\mathbf U \to \Bbb F$.
Hence $\mathbf U \subsetneq \Bbb F$.
Hence $\exists f \in \Bbb F: f \notin \mathbf U$.
Category:Primitive Recursive Functions
Not All URM Computable Functions are Primitive Recursive

== Theorem ==
There exist URM computable functions which are not primitive recursive.
== Proof ==
Consider the basic primitive recursive functions.
To each basic primitive recursive function $f$ let us assign a code number $\map \delta f$, as follows:
* $\map \delta {\operatorname{zero} } = 3$
* $\map \delta {\operatorname{succ} } = 9$
* $\forall k, m \in \N^*: m \le k: \map \delta {\pr^k_m} = 2^k 3^m$
Suppose the function $h$ is defined by substitution from the functions $f, g_1, g_2, \ldots, g_t$ to which we have already assigned code numbers.
Then we put:
:$\map \delta h = 2^{\map \delta f} 3^{\map \delta {g_1} } 5^{\map \delta {g_2} } \cdots p_{t + 1}^{\map \delta {g_t} } + 1$
Suppose the function $h$ is defined by primitive recursion from the functions $f$ and $g$ to which we have already assigned code numbers.
Then we put:
:$\map \delta h = 2^{\map \delta f} 3^{\map \delta g} + 2$
Thus we assign a code number to every definition of a primitive recursive function.
Given any natural number $m$ we can determine whether $m$ is the code number for a definition of a primitive recursive function, and if so, work out what definition it encodes.
In particular, given any such $m$ we can work out whether it encodes a primitive recursive function $f: \N \to \N$, and determine how $f$ is built up from basic primitive recursive functions on up.
From this definition, we can compute all the values of $f$ for all inputs $n \in \N$.
So, we define the function $\Phi: \N^2 \to \N$ as follows:
:$\map \Phi {m, n} = \begin{cases}
\map f n & : \text{if } m \text { codes a definition of the primitive recursive function } f: \N \to \N \\
0 & : \text{otherwise}
\end{cases}$
It is deducible by arguments derived from proofs of the various primitive recursive functions that there is a URM program for computing the values of $\Phi$.
That is, $\Phi$ can be shown to be URM computable
Now we apply Cantor's Diagonal Argument to create the following URM computable function $g: \N \to \N$:
:$\map g n = \map \Phi {n, n} + 1$
We have that $\Phi$ is URM computable.
So it follows that $\map g n$ is also URM computable.
Now, let $f$ be a primitive recursive function and let $m$ code some definition of $f$.
So, for all $n \in \N$, we have:
:$\map f n = \map \Phi {m, n}$
Thus $\map f m = \map \Phi {m, m}$.
Now, since $\map g m = \map \Phi {m, m} + 1$, we see that $\map g m \ne \map f m$, whatever $f$ may happen to be.
Hence $g \ne f$.
So $g$ is different from any primitive recursive function $f$ that we care to devise.
Therefore $g$ is a URM computable function which is not primitive recursive.
Hence the result.
Category:URM Programs
Category:Primitive Recursive Functions
Not Coprime means Common Prime Factor

== Theorem ==
Let $a, b \in \Z$.
If $d \divides a$ and $d \divides b$ such that $d > 1$, then $a$ and $b$ have a common divisor which is prime.
== Proof ==
As $d > 1$, it has a prime decomposition.
Thus there exists a prime $p$ such that $p \divides d$.
From Divisor Relation on Positive Integers is Partial Ordering, we have $p \divides d, d \divides a \implies p \divides a$, and similarly for $b$.
The result follows.
Category:Coprime Integers
Category:Prime Numbers
Not Every Class is a Set/Proof 1

== Theorem ==
== Proof ==
Let a set $x$ be defined as ordinary $x \notin x$.
Let $\map \phi x$ be the set property defined as:
:$\map \pi x := \neg \paren {x \in x}$
Then by the axiom of specification there exists a class, which can be denoted $A$, such that:
:$A = \set {x: \neg \paren {x \in x} }$
By the axiom of extension $A$ is unique.
Thus $A$ is the class of all ordinary sets.
Hence we have:
:$x \in A \iff x \notin x$
 $A$ were a set.
Then we could set $A$ for $x$, and so obtain:
:$A \in A \iff A \notin A$
This is a contradiction.
Hence by Proof by Contradiction $A$ cannot be a set.
But as $A$ is a subclass of the universal class $V$, $A$ is a class.
So the class $A$ of ordinary sets is not a set.
That is:
:$A \notin V$
== Sources ==
* : Chapter $2$: Some Basics of Class-Set Theory: $\S 1$ Extensionality and separation: Theorem $1.1$
Category:Not Every Class is a Set
Not Every Class is a Set/Proof 2

== Theorem ==
== Proof ==
Consider the universal class $V$.
From Class has Subclass which is not Element, $V$ has a subclass $A$ which is not an element of $V$.
But $V$ contains as elements all the sets.
It follows that $A$ is a class which is not a set.
== Sources ==
* : Chapter $2$: Some Basics of Class-Set Theory: $\S 1$ Extensionality and separation: Theorem $1.1$
Category:Not Every Class is a Set
Not Every Class is a Set/Proof 3

== Theorem ==
== Proof ==
Suppose $A$ is the universal class, which is a fortiori a class.
The result follows from Basic Universe is not Set.
== Sources ==
* : Chapter $2$: Some Basics of Class-Set Theory: $\S 1$ Extensionality and separation: Theorem $1.1$
Category:Not Every Class is a Set
Not Every Horizontal Vector Field is Horizontal Lift

== Theorem ==
Let $\pi : \R^2 \to \R$ be the projection map such that:
:$\map \pi {x, y} = x$
Let $W = y \partial_x$ be a smooth vector field on $\R^2$.
Then $W$ is horizontal, but there is no smooth vector field whose horizontal lift is equal to $W$.
== Proof ==
== Sources ==
* : $\S 2$: Riemannian Metrics. Methods for Constructing Riemannian Metrics
Category:Riemannian Geometry
Not Every Number is the Sum or Difference of Two Prime Powers

== Theorem ==
Not every positive integer can be expressed in the form $p^m \pm q^n$ where $p, q$ are prime and $m, n$ are positive integers.
== Proof ==
What is to be demonstrated is that there exist odd integers which cannot be expressed as $2^m \pm q^n$.
== Sources ==
* 
Category:Not Every Number is the Sum or Difference of Two Prime Powers
Not Every Two-Person Zero-Sum Game has Saddle Point

== Theorem ==
Not every two-person zero-sum game has a saddle point.
== Proof ==
Consider the game of Matching Pennies.
Recall its payoff table:
Trivially, by inspection, this has no entry which is the smallest entry in its row and the largest entry in its column.
== Sources ==
* : Chapter $\text{I}$: An Outline of the Theory of Games: $3$
Category:Two-Person Zero-Sum Games
Not Preceding implies Approximating Relation and not Preceding

== Theorem ==
Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $x, y \in S$ such that
:$x \npreceq y$
Let $\RR$ be an approximating relation on $S$.
Then
:$\exists u \in S: \tuple {u, x} \in \RR \land u \npreceq y$
== Proof ==
By definition of approximating relation:
:$x = \map \sup {x^\RR}$
By definition of supremum:
:$y$ is upper bound for $x^\RR \implies x \preceq y$
By definition of upper bound:
:$\exists u \in S: u \in x^\RR \land u \npreceq y$
Thus by definition of $\RR$-segment:
:$\exists u \in S: \tuple {u, x} \in \RR \land u \npreceq y$
== Sources ==
* 
* 
Category:Approximating Relations
Category:Complete Lattices
Not Preceding implies Exists Completely Irreducible Element in Algebraic Lattice

== Theorem ==
Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below algebraic lattice.
Let $x, y \in S$ such that
:$y \npreceq x$
Then
:$\exists p \in S: p$ is completely irreducible $\mathop \land x \preceq p \land y \npreceq p$
== Proof ==
By definition of algebraic:
:$\forall z \in S: z^\ll$ is directed
and
:$L$ satisfies the axiom of approximation.
By Axiom of Approximation in Up-Complete Semilattice:
:$\exists k \in S: k \ll y \land k \npreceq x$
By Algebraic iff Continuous and For Every Way Below Exists Compact Between:
:$\exists z \in \map K L: k \preceq z \preceq y$
By definition of transitivity:
:$z \npreceq x$
By definition of upper closure of element:
:$x \notin z^\succeq$
By definition of difference:
:$x \in S \setminus z^\succeq$
By definition of relative complement:
:$x \in \relcomp S {z^\succeq}$
By definition of compact subset:
:$z$ is a compact element.
By Upper Closure of Element is Way Below Open Filter iff Element is Compact:
:$z^\succeq$ is a way below open filter on $L$.
By Upper Way Below Open Subset Complement is Non Empty implies There Exists Maximal Element of Complement:
:$\exists p \in S: x \preceq p \land p = \max \relcomp S {z^\succeq}$
Thus by Maximal implies Completely Irreducible:
:$p$ is completely irreducible.
Thus:
:$x \preceq p$
:
:$y \preceq p$
By definition of transitivity:
:$z \preceq p$
By definition of maximum element:
:$p \in \relcomp S {z^\succeq}$
By definition of relative complement:
:$p \notin z^\succeq$
Thus this contradicts $z \preceq p$ by definition of upper closure of element.
== Sources ==
* 
Category:Continuous Lattices
Category:Meet Irreducible Elements