nyuuzyou/wikis huggingface dataset:
Ellipse is Bounded in Plane

== Theorem ==
Let $E$ be an ellipse embedded in in a Euclidean plane.
Then $E$ is bounded.
== Proof ==
Let a Cartesian coordinate system be applied to the Euclidean plane in which $E$ is embedded.
Let $E$ be expressed in reduced form:
Hence:
:there are no real values of $x$ for $\size y > b$
:there are no real values of $y$ for $\size x > b$.
Hence $E$ exists entirely within the rectangle whose sides are $x = \pm a$ and $y = \pm b$.
The result follows.
== Sources ==
* : Chapter $\text {IV}$. The Ellipse: $2$. To find the equation of the ellipse in its simplest form
Category:Ellipses
Elliptic Curve/Examples/Arbitrary Example 1

== Example of Elliptic Curve ==
:
The equation:
:$y^2 = x^3 + 17$
describes an elliptic curve.
This has the rational lattice points $\tuple {-2, 3}$, $\tuple {2, 5}$, $\tuple {\dfrac 1 4, \dfrac {33} 8}$, $\tuple {-1, 4}$ and many more.
== Sources ==
* 
Category:Examples of Elliptic Curves
Elliptic Curve/Examples/Arbitrary Example 1/Mistake

== Source Work ==
:
:
:elliptic curve
== Mistake ==
For example, the elliptic curve $y^2 = x^3 + 17$ has a rational point $\tuple {-2, 3}$, but it also has many others, e.g. $\tuple {2, 3}$, $\tuple {\frac 1 4, \frac {33} 8}$, and $\tuple {-1, 4}$.
== Correction ==
$\tuple {2, 3}$ is not a rational point of $y^2 = x^3 + 17$.
We find that:
:$2^3 + 17 = 25$
from which it follows that the rational point in question is actually $\tuple {2, 5}$.
This section does not appear in the second edition.
== Sources ==
* 
Category:Mistakes/The Penguin Dictionary of Mathematics
Elliptic Function/Examples/First Kind

== Examples of Elliptic Functions ==
Consider the incomplete elliptic integral of the first kind:
:$u = \ds \int_0^x \dfrac {\d t} {\sqrt {\paren {1 - t^2} \paren {1 - k^2 t^2} } }$
Then we have the following elliptic functions:
== Also see ==
Compare with:
:$x = \sin u$
where:
:$\ds u = \int_0^x \dfrac {\d t} {\sqrt {1 - t^2} }$
== Sources ==
* 
* 
Category:Examples of Elliptic Functions
Eluding Game has no Saddle Point

== Theorem ==
The eluding game has no saddle point.
== Proof ==
Recall the 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
Embedded Smooth Hypersurface from Regular Points of Smooth Function

== Theorem ==
Let $\struct {M, g}$ be a Riemannian manifold.
Let $f \in \map {C^\infty} M$ be a smooth function.
Let $R \subseteq M$ be the set of regular points of $f$.
Let $c \in \R$.
Let $M_c$ be a set such that:
:$M_c = \map {f^{-1} } c \cap R$
Suppose $M_c$ is non-empty.
Then $M_c$ is an embedded smooth hypersurface in $M$.
Furthermore, the gradient $\grad f$ is everywhere normal to $M_c$.
== Proof ==
== Sources ==
* : $\S 2$: Riemannian Metrics. Basic Constructions on Riemannian Manifolds
Category:Riemannian Geometry
Embedding Division Ring into Quotient Ring of Cauchy Sequences

== Theorem ==
Let $\struct {R, \norm {\, \cdot \,} }$ be a normed division ring.
Let $\CC$ be the ring of Cauchy sequences over $R$
Let $\NN = \set {\sequence {x_n}: \ds \lim_{n \mathop \to \infty} x_n = 0}$
Let $\norm {\, \cdot \,}: \CC \, \big / \NN \to \R_{\ge 0}$ be the norm on the quotient ring $\CC \, \big / \NN$ defined by:
:$\ds \forall \sequence {x_n} + \NN: \norm {\sequence {x_n} + \NN} = \lim_{n \mathop \to \infty} \norm {x_n}$
Let $\phi: R \to \CC \, \big / \NN$ be the mapping from $R$ to the quotient ring $\CC \, \big / \NN$ defined by:
:$\forall a \in R: \map \phi a = \sequence {a, a, a, \dotsc} + \NN$
where $\sequence {a, a, a, \dotsc} + \NN$ is the left coset in $\CC \, \big / \NN$ that contains the constant sequence $\sequence {a, a, a, \dotsc}$.
Then:
:$\phi$ is a distance-preserving ring monomorphism.
== Proof ==
By the definition of a distance-preserving mapping and a ring monomorphism it has to be shown that:
:$(1): \quad \phi$ is a homomorphism.
:$(2): \quad \phi$ is an injection.
:$(3): \quad \phi$ is distance-preserving.
=== $(1): \quad \phi$ is a homomorphism ===
By definition, $\phi$ is the composition of two mappings:
:$\phi = q \circ \phi'$
where:
:$\text{(a)}: \quad \phi': R \to \CC$, defined by: $\forall a \in R, \map {\phi'} a = \sequence {a, a, a, \dotsc}$
:$\text{(b)}: \quad q$ is the quotient mapping $q: \CC \to \CC \, \big / \NN$ defined by: $\map q {\sequence {x_n} } = \sequence {x_n} + \NN$
By Embedding Normed Division Ring into Ring of Cauchy Sequences, $\phi'$ is a ring monomorphism.
By Quotient Ring Epimorphism is Epimorphism, then $q$ is a ring epimorphism.
By Composition of Ring Homomorphisms is Ring Homomorphism then the composition $\phi = q \circ \phi'$ is a ring homomorphism
=== $(2): \quad \phi$ is an injection ===
Let $a, b \in R$.
Suppose $\map \phi a = \map \phi b$.
Then:
By Constant Sequence Converges to Constant in Normed Division Ring then:
:$\ds \lim_{n \mathop \to \infty} {a - b} = a - b$
Hence $a-b = 0$.
The result follows.
=== $(3): \quad \phi$ is distance-preserving ===
Let $a, b \in R$.
Then:
== Sources ==
* : $\S 3.2$: Completions: Problem $85$
Category:Cauchy Sequences
Category:Normed Division Rings
Embedding Normed Division Ring into Ring of Cauchy Sequences

== Theorem ==
Let $\struct {R, \norm {\, \cdot \,} }$ be a normed division ring.
Let $\CC$ be the ring of Cauchy sequences over $R$
Let $\phi: R \to \CC$ be the mapping from $R$ to $\CC$ defined as:
:$\forall a \in R: \map \phi a = \tuple {a, a, a, \dots}$
where $\tuple {a, a, a, \dots}$ is the constant sequence.
Then $\phi$ is a ring monomorphism.
== Proof ==
By Cauchy Sequences form Ring with Unity, $\CC$ is a subring of the ring of sequences over $R$.
Let $i: \CC \to R^\N$ be the inclusion mapping of $\CC$ into the ring of sequences.
By Embedding Ring into Ring Structure Induced by Ring Operations the composition $i \circ \phi: R \to R^\N$ is a ring monomorphism.
Since for all $a \in R$, we have that:
:$\map {\paren {i \circ \phi} } a = \map \phi a$
The result follows.
== Sources ==
Category:Cauchy Sequences
Category:Normed Division Rings
Embedding Ring into Ring Structure Induced by Ring Operations

== Theorem ==
Let $\struct {R, +, \circ}$ be a ring.
Let $S$ be a non-empty set.
Let $\struct {R^S, +', \circ'}$ be the ring of mappings, where $+'$ and $\circ'$ are the pointwise operations induced on $R^S$ by $+$ and $\circ$.
For each $r \in R$, let $f_r: S \to R$ be the mapping defined by:
:$\forall s \in S, \map {f_r} s = r$
That is, $f_r$ is the constant mapping from $S$ to $r$.
Let $\phi: R \to R^S$ be the mapping from the ring $R$ to the ring $R^S$ defined by:
:$\forall r \in R: \map \phi r = f_r$
Then:
:$\phi$ is a ring monomorphism.
== Proof ==
By the definition of a ring monomorphism it is sufficient to prove for all $r, r' \in R$ that:
:$\quad \map \phi {r + r'} = \map \phi r +' \map \phi {r'}$
:$\quad \map \phi {r \circ r'} = \map \phi r \circ' \map \phi {r'}$
:$\quad r \ne r' \implies \map \phi r \ne \map \phi {r'}$
That is, for all $r, r' \in R$ it needs to be shown that:
:$(1): \quad f_{r + r' } = f_r +' f_{r'}$
:$(2): \quad f_{r \circ r' } = f_r \circ' f_{r'}$
:$(3): \quad r \ne r' \implies f_r \ne f_{r'}$
=== $(1): f_{r + r'} = f_r +' f_{r'}$ ===
For all $s \in S$:
The result follows.
=== $(2): f_{r \circ r'} = f_r \circ' f_{r'}$ ===
For all $s \in S$:
The result follows.
=== $(3): r \ne r' \implies f_r \ne f_{r'}$ ===
Let $s \in S$, then:
:$\map {f_r} s = r \ne r' = \map {f_{r'} } s$
So:
:$f_r \ne f_{r'}$
and the proof is complete.
Category:Rings of Mappings
Category:Ring Monomorphisms
Embedding Theorem/Corollary

== Corollary to Embedding Theorem ==
Let:
:$(1): \quad \struct {T_2, \oplus_2, \otimes_2}$ be a submagma of $\struct {S_2, *_2, \star_2}$
:$(2): \quad f: \struct {T_1, \oplus_1, \otimes_1} \to \struct {T_2, \oplus_2, \otimes_2}$ be an isomorphism
then there exists:
:$(1): \quad$ a magma $\struct {S_1, *_1, \star_1}$ which algebraically contains $\struct {T_1, \oplus_1, \otimes_1}$
:$(2): \quad g: \struct {S_1, *_1, \star_1} \to \struct {S_2, *_2, \star_2}$ where $g$ is an isomorphism which extends $f$.
== Proof ==
By the Embedding Theorem, there exists:
:a magma $\struct {S_1, *_1}$ which algebraically contains $\struct {T_1, \oplus_1}$
:an isomorphism $g: \struct {S_1, *_1} \to \struct {S_2, *_2}$ which extends $f$.
Let $\star_1$ be the transplant of $\star_2$ under $g^{-1}$.
We have that:
:$g^{-1}$ is an isomorphism from $\struct {S_2, \star_2}$ to $\struct {S_1, \star_1}$.
Hence:
:$g$ is an isomorphism from $\struct {S_1, \star_1}$ to $\struct {S_2, \star_2}$.
It follows that:
:$g$ is an isomorphism from $\struct {S_1, *_1, \star_1}$ to $\struct {S_2, *_2, \star_2}$.
It remains to be shown that:
:$\struct {T_1, \otimes_1}$ is closed
and:
:the operation induced on $T_1$ by $\star_1$ is $\otimes_1$.
Let $x, y \in T_1$.
Then:
:$\map g x = \map f x$
and:
:$\map g y = \map f y$
such that:
:$\map g x, \map g y \in T_2$
So by definition of $\star_1$:
Hence $\struct {T_1, \oplus_1, \otimes_1}$ is embedded in $\struct {S_1, *_1, \star_1}$.
== Sources ==
* : Chapter $\text {II}$: New Structures from Old: $\S 8$: Compositions Induced on Subsets: Theorem $8.1$
Category:Embedding Theorem
Embedding Theorem/Motivation

== Motivation for Embedding Theorem ==
The following is a frequently occurring circumstance in the field of abstract algebra.
:We have a magma $\struct {T_1, \circ}$.
:$\struct {T_1, \circ}$ is isomorphic to another magma $\struct {T_2, *}$.
:$\struct {T_2, *}$ is embedded in a magma $\struct {S_2, *}$.
:We want to embed $\struct {T_1, \circ}$ in its own magma $\struct {S_1, \circ}$ such that $\struct {S_1, \circ} \cong \struct {S_2, *}$.
This can always be done, as the Embedding Theorem theorem shows.
== Sources ==
* : Chapter $\text {II}$: New Structures from Old: $\S 8$: Compositions Induced on Subsets: Theorem $8.1$
Category:Embedding Theorem
Empty Class Exists and is Unique

== Theorem ==
There is exactly one empty class.
== Proof ==
Let $P$ be a property such that $\map P x$ is satisfied by no $x$ at all, for example:
:$\forall x: \map P x := \neg {x = x}$
Then by the Axiom of Specification we can create the class $A$ such that:
:$A := \set {x \in V \land \neg {x = x} }$
from which it is seen that $A$ has no elements.
Hence there exists an empty class.
Let $A$ and $B$ both be empty classes.
By definition, both $A$ and $B$ contain the same elements, that is, no elements at all.
By the Axiom of Extension, that means $A = B$.
Hence the result.
== Also see ==
* Empty Set is Unique
== Sources ==
* : Chapter $2$: Some Basics of Class-Set Theory: $\S 3$ Axiom of the empty set
Category:Empty Class
Empty Class is Subclass of All Classes

== Theorem ==
The empty class is a subclass of all classes.
== Proof ==
Let $A$ be a class.
By definition of the empty class:
:$\forall x: \neg \paren {x \in \O}$
From False Statement implies Every Statement:
:$\forall x: \paren {x \in \O \implies x \in A}$
Hence the result by definition of subclass.
== Sources ==
* : Chapter $2$: Some Basics of Class-Set Theory: $\S 3$ Axiom of the empty set: Note $1$.
Category:Empty Class
Empty Class is Supercomplete

== Theorem ==
The empty class is supercomplete.
== Proof ==
Vacuously, every element of $\O$ is also a subclass of $\O$.
Hence $\O$ is transitive by definition.
Vacuously, every subclass of every element of $\O$ is also an element of $\O$.
Hence $\O$ is swelled by definition.
The result follows by definition of supercomplete.
== Sources ==
* : Chapter $2$: Some Basics of Class-Set Theory: $\S 3$ Axiom of the empty set: Note $2$.
Category:Empty Class
Category:Supercomplete Classes
Empty Class is Transitive

== Example of Transitive Class ==
The empty class is transitive.
== Proof ==
Vacuously, every element of $\O$ is also a subclass of $\O$.
Hence $\O$ is transitive by definition.
== Sources ==
* : Chapter $2$: Some Basics of Class-Set Theory: $\S 10$ Some useful facts about transitivity
Category:Examples of Transitive Classes
Category:Empty Class
Empty Class is Well-Ordered

== Theorem ==
Let $V$ be a basic universe.
Let $\RR \subseteq V \times V$ be a relation.
Let $\O$ denote the empty class.
Then $\O$ is well-ordered under $\RR$.
== Proof ==
We have that $\O$ is well-ordered under $\RR$ every non-empty subclass of $\O$ has a smallest element under $\RR$.
But $\O$ has no non-empty subclass.
Hence this condition is satisfied vacuously.
The result follows.
Category:Empty Class
Category:Well-Orderings
Empty Group Word is Reduced

== Theorem ==
Let $S$ be a set
Let $\epsilon$ be the empty group word on $S$.
Then $\epsilon$ is reduced.
== Proof ==
By definition, a group word $w = w_1 \cdots w_i \cdots w_n$ is reduced :
:$w_i \ne {w_{i + 1} }^{-1}$ for all $i \in \set {1, \ldots, n - 1}$
where $w_1, w_2, \ldots$ are elements of $S$.
We have that $\epsilon$ is the empty group word on $S$.
Hence by definition it has no elements of $S$ in it.
Hence the condition for $\epsilon$ to be reduced is vacuously true.
Category:Group Words
Empty Intersection iff Subset of Complement

== Corollary to Intersection with Complement is Empty iff Subset ==
:$S \cap T = \O \iff S \subseteq \relcomp {} T$
where:
:$S \cap T$ denotes the intersection of $S$ and $T$
:$\O$ denotes the empty set
:$\complement$ denotes set complement
:$\subseteq$ denotes subset.
=== Corollary ===
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : $\S 1$. Sets; inclusion; intersection; union; complementation; number systems: Exercise $11 \ \text{(b)}$
* : Chapter $1$: Theory of Sets: $\S 3$: Set Operations: Union, Intersection and Complement: Exercise $1 \ \text{(c)}$
Category:Set Complement
Category:Set Intersection
Category:Empty Set
Category:Subsets
Category:Empty Intersection iff Subset of Complement
Empty Intersection iff Subset of Complement/Corollary

== Corollary to Empty Intersection iff Subset of Complement ==
Let $A, B, S$ be sets such that $A, B \subseteq S$.
Then:
:$\exists X \in \powerset S: \paren {A \cap X} \cup \paren {B \cap \complement_S \paren X} = \O \iff A \cap B = \O$
where $\overline X$ denotes the relative complement of $X$ in $S$.
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : Chapter $1$: Sets and Logic: Exercise $6$
Category:Set Union
Category:Set Intersection
Category:Set Complement
Category:Empty Intersection iff Subset of Complement
Empty Intersection iff Subset of Complement/Corollary/Proof 2

== Corollary to Empty Intersection iff Subset of Complement ==
== Proof ==
We have:
:result $\paren {A \cap C} \cup \paren {B \cap \map \complement C} = \O \iff B \subseteq C \subseteq \map \complement A$:
where the universe $\Bbb U$ is posited.
Let $S$ take the position of $\Bbb U$.
Let $C = X$.
Then we have:
:$\paren {A \cap X} \cup \paren {B \cap \relcomp S X} = \O \iff B \subseteq X \subseteq \relcomp S A$
Thus we have shown that:
:$B \subseteq \relcomp S A$
and it follows from Empty Intersection iff Subset of Complement that:
:$A \cap B = \O$
Category:Empty Intersection iff Subset of Complement
Empty Intersection iff Subset of Complement/Proof 2

== Corollary to Intersection with Complement is Empty iff Subset ==
== Proof ==
From Intersection with Complement is Empty iff Subset
:$S \subseteq T \iff S \cap \relcomp {} T = \O$
Then we have:
Thus:
== Sources ==
* : Chapter $1$: Sets and Logic: Exercise $6$
Category:Empty Intersection iff Subset of Complement
Empty Intersection iff Subset of Relative Complement

== Theorem ==
Let $S$ be a set.
Let $A, B$ be subset of $S$.
Then $A \cap B = \O \iff A \subseteq \relcomp S B$
== Proof ==
:$A \cap B = \O$
:$\forall x \in S: x \notin A \cap B$ by Empty Set as Subset
:$\forall x \in S: \neg \paren {x \in A \land x \in B}$ by definition of intersection
:$\forall x \in S: x \notin A \lor x \notin B$ by De Morgan's Laws (Logic)/Disjunction of Negations
:$\forall x \in S: x \in A \implies x \notin B$ by Rule of Material Implication
:$\forall x \in S: x \in A \implies x \in \relcomp S B$ by definition of relative complement
:$A \subseteq \relcomp S B$ by Subset in Subsets.
== Sources ==
* 
Category:Relative Complement
Category:Set Intersection
Category:Empty Set
Category:Subsets
Empty Mapping is Mapping

== Theorem ==
For each set $T$, the empty mapping, where the domain is the empty set, is a mapping.
== Proof ==
Let $e: \O \to T$ be the empty mapping.
Vacuously:
:$\forall x \in \O: \exists y \in T: \tuple {x, y} \in e$
thus showing that $e$ is left-total.
Also vacuously:
:$\forall x \in \O: \forall y_1, y_2 \in T: \tuple {x, y_1} \in e \land \tuple {x, y_2} \in e \implies y_1 = y_2$
thus showing that $e$ is many-to-one.
Hence the result, from the definition of a mapping.
== Sources ==
* : Chapter $\text{I}$: Sets and Functions: Functions
Category:Empty Mapping
Empty Mapping is Surjective iff Codomain is Empty

== Theorem ==
Let $T$ be a set.
Let $\O$ denote the empty set.
Let $e: \O \to T$ be the empty mapping.
Then $e$ is a surjection $T = \O$.
== Proof ==
Let $T = \O$.
From Empty Mapping to Empty Set is Bijective, $e$ is a bijection.
Hence $e$ is a surjection.
Let $T \ne \O$.
 $e$ is a surjection.
Let $t \in T$.
As $e$ is a surjection:
:$(1): \quad \exists s \in S: \map e s = t$
But by Null Relation is Mapping iff Domain is Empty Set:
:$\Dom e = \O$
Hence:
:$\nexists s \in S: \map e s = t$
This is a contradiction of $(1)$.
Hence by Proof by Contradiction it is not possible for $e$ to be a surjection.
Hence if $e$ is a surjection it must be the case that $T = \O$.
So we have:
:$T = \O$ implies that $e$ is a surjection
:$e$ is a surjection implies that $T = \O$
and the result follows.
Category:Empty Mapping
Category:Surjections
Empty Mapping is Unique

== Theorem ==
For each set $T$ there exists exactly one empty mapping $e: \O \to T$ whose domain is the empty set.
== Proof ==
By definition a mapping from $\O$ to $T$ is a subset of the cartesian product $\O \times T$:
:$e: \O \to T \subseteq \O \times T$
From Empty Mapping is Mapping, we have that the empty mapping from $\O$ to $T$ exists.
From Cartesian Product is Empty iff Factor is Empty it follows that the empty mapping equals the empty set:
:$\O \times T = \O$
The result follows by Empty Set is Unique.
== Sources ==
* : Chapter $\text{I}$: Sets and Functions: Functions
Category:Empty Mapping
Empty Mapping to Empty Set is Bijective

== Theorem ==
Let $\nu: \O \to \O$ be an empty mapping.
Then $\nu$ is a bijection.
== Proof 1==
From Empty Mapping is Injective, $\nu$ is injective.
As the codomain of $\nu$ is empty, $\nu$ is vacuously surjective.
== Proof 2==
From Empty Mapping is Injective, $\nu$ is injective.
As the codomain of $\nu$ is empty, from Empty Mapping is Surjective iff Codomain is Empty, we have that $\nu$ is surjective.
Hence the result.
Category:Bijections
Category:Empty Mapping
Empty Product is Terminal Object

== Theorem ==
Let $\mathbf C$ be a metacategory.
Suppose $\mathbf C$ admits a product $\prod \O$ for the empty set.
Then $\prod \O$ is a terminal object of $\mathbf C$.
== Proof ==
By definition, $\prod \O$ is the limit of the empty subcategory $\mathbf 0$ of $\mathbf C$.
The result follows from Terminal Object as Limit.
Category:Limits and Colimits
Category:Category Theory
Empty Set/Examples/Real Roots of x^2 + 1

== Example of Empty Set ==
The set:
:$S = \set {x \in \R: x^2 + 1 = 0}$
is an instance of a specification of the empty set.
== Proof ==
From Existence of Real Polynomial with no Real Root, there exists no $x \in \R$ such that $x^2 + 1 = 0$.
Hence the result.
== Sources ==
* : $\S 1$: Real Numbers: $\S 1.1$: Set Notation
Category:Examples of Empty Sets
Empty Set Satisfies Topology Axioms

== Theorem ==
Let $T = \struct {\O, \set \O}$ where $\O$ denotes the empty set.
Then $T$ satisfies the open set axioms for a topological space.
== Proof ==
We proceed to verify the open set axioms for $\set \O$ to be a topology on $\O$.
Let $\tau = \set \O$.
=== ===
By Union of Empty Set:
:$\ds \bigcup \tau = \O \in \tau$
Thus is satisfied.
=== ===
From Intersection with Empty Set:
:$\O \cap \O = \O \in \tau$
and so is satisfied.
=== ===
By definition $\O \in \tau$ and so is satisfied.
All the open set axioms are fulfilled, and the result follows.
Category:Topology
Category:Empty Set
Category:Empty Topological Space
Empty Set and Set form Algebra of Sets

== Theorem ==
Let $S$ be any non-empty set.
Then $\set {S, \O}$ is (trivially) an algebra of sets, where $S$ is the unit.
== Proof ==
From Set Union is Idempotent:
:$S \cup S = S$
and
:$\O \cup \O = \O$
Then from Union with Empty Set:
:$S \cup \O = S$
So $\set {S, \O}$ is closed under union.
From Relative Complement of Empty Set:
:$\relcomp S \O = S$
and from Relative Complement with Self is Empty Set:
:$\relcomp S S = \O$
so $\set {S, \O}$ is closed under complement.
Hence the result, by definition of algebra of sets.
Category:Algebras of Sets
Empty Set as Subset

== Theorem ==
Let $S$ be a set.
Let $A$ be a subset of $S$.
Then:
:$A = \O \iff \forall x \in S: x \notin A$
== Proof ==
Sufficient condition follows by definition of empty set.
For necessary condition assume that:
:$\forall x \in S: x \notin A$
Let $x$ be arbitrary.
 that:
:$x \in A$
By definition of subset:
:$x \in S$
By assumption:
:$x \notin A$
Thus this contradicts:
:$x \in A$
Category:Empty Set
Category:Subsets
Empty Set can be Derived from Axiom of Abstraction

== Theorem ==
The empty set can be formed by application of the .
Hence the empty set can be derived as a valid object in Frege set theory.
== Proof ==
Let $P$ be the property defined as:
:$\forall x: \map P x := \neg \paren {x = x}$
Hence, using the , we form the set:
:$\O := \set {x: \neg \paren {x = x} }$
where the property ${\map P x}$ is:
:$\neg \paren {x = x}$
Since we have that:
:$\forall x: x = x$
it is seen that $\O$ as defined here has no elements.
By definition of Frege set theory, given any property $P$, there exists a unique set which consists of all and only those objects which have property $P$:
:$\set {x: \map P x}$
Therefore, there exists a unique set
:$\O := \set {x: \neg \paren {x = x} }$
which the property $P= \neg \paren {x = x}$, which consists of no elements.
Hence, by the definition of the empty set, this set is a valid object in Frege set theory.
Hence the result by definition of the empty set.
== Sources ==
* : Chapter $1$: General Background: $\S 7$ Frege set theory
Category:Empty Set
Category:Axiom of Abstraction
Empty Set forms Formal Language

== Example of Formal Language ==
The empty set $\O$ forms a formal language.
== Proof ==
$\O$ vacuously forms a set of symbols.
Similarly, the formal grammar is vacuous.
The result follows by definition of formal language.
== Also see ==
* Set of Null Strings forms Formal Language: a different formal language from this one
== Sources ==
* : Chapter $1$: Preliminaries: $1.1$ Strings, Alphabets and Languages
Category:Examples of Formal Languages
Category:Empty Set
Empty Set from Principle of Non-Contradiction

== Theorem ==
The empty set can be characterised as:
:$\O := \set {x: x \in E \text { and } x \notin E}$
where $E$ is an arbitrary set.
== Proof ==
 $x \in \O$ as defined here.
Thus we have:
:$x \in E$
and:
:$x \notin E$
This is a contradiction.
It follows by Proof by Contradiction that $x \notin \O$.
Hence, as $x$ was arbitrary, there can be no $x$ such that $x \in \O$.
Thus $\O$ is the empty set by definition.
== Sources ==
* : $\S 1$. Sets; inclusion; intersection; union; complementation; number systems
Category:Empty Set
Empty Set is Bottom of Lattice of Power Set

== Theorem ==
Let $X$ be a set.
Let $L = \struct {\powerset X, \cup, \cap, \subseteq}$ be the lattice of the power set of $X$.
Then:
:$\O = \bot$
where $\bot$ denotes the bottom of $L$.
== Proof ==
By Empty Set is Subset of All Sets:
:$\forall S \in \powerset X: \O \subseteq S$
By Empty Set is Element of Power Set:
:$\O \in \powerset X$
Thus by definition of the smallest element:
:$\O = \bot$
== Sources ==
* 
* 
* 
Category:Lattice Theory
Category:Power Set
Empty Set is Closed/Metric Space

== Theorem ==
Let $M = \struct {A, d}$ be a metric space.
Then the empty set $\O$ is closed in $M$.
== Proof ==
From Metric Space is Open in Itself, $A$ is open in $M$.
But:
:$\O = \relcomp A A$
where $\complement_A$ denotes the set complement relative to $A$.
The result follows by definition of closed set.
== Sources ==
* : Chapter $2$: Metric Spaces: $\S 6$: Open Sets and Closed Sets
Category:Closed Sets (Metric Spaces)
Category:Empty Set is Closed