nyuuzyou/wikis huggingface dataset:
Tychonoff's Theorem/General Case/Proof 1

== Theorem ==
== Proof ==
First assume that $X$ is compact. 
From Projection from Product Topology is Continuous, the projections $\pr_i : X \to X_i$ are continuous.
It follows from Continuous Image of Compact Space is Compact that the $X_i$ are compact.
Assume now that each $X_i$ is compact.
By Equivalence of Definitions of Compact Topological Space it is enough to show that every ultrafilter on $X$ converges.
Thus let $\FF$ be an ultrafilter on $X$.
From Image of Ultrafilter is Ultrafilter, for each $i \in I$, the image filter $\map {\pr_i} \FF$ is an ultrafilter on $X_i$.
Each $X_i$ is compact by assumption.
So by Equivalence of Definitions of Compact Topological Space, each $\map {\pr_i} \FF$ converges.
By Filter on Product Space Converges iff Projections Converge, $\FF$ converges.
Category:Tychonoff's Theorem
Tychonoff's Theorem/General Case/Proof 2/Lemma 1

== Lemma ==
Let $X$ be a set.
We say that a family $\CC$ of subsets of $X$ has the "finite intersection property" if:
:$\ds \bigcap_{S \in \SS} S \ne \O$
for all finite subsets $\SS \subseteq \CC$.
Let: 
:$\ds S = \set {\CC \subseteq \AA : \AA \text { has the finite intersection property} }$
Then $S$ has a $\subseteq$-maximal element $\AA$.
== Proof ==
We will use Zorn's Lemma for this.
Clearly $S \ne \O$, since $\CC \in S$. 
Now let $\family {U_\alpha}_{\alpha \mathop \in A}$ be a non-empty chain in $S$.
Let:
:$\ds U = \bigcup_{\alpha \mathop \in A} U_\alpha$ 
We have $U_\alpha \subseteq U$ for each $\alpha \in A$. 
It remains to show that $U$ has the finite intersection property.
Let $F \subseteq U$ be a finite set, and write: 
:$F = \set {C_1, C_2, \ldots, C_n}$ 
For each $1 \le i \le n$, pick $\alpha_i \in A$ such that: 
:$C_i \in U_{\alpha_i}$
Since $\family {U_\alpha}_{\alpha \mathop \in A}$ is a chain, there exists $1 \le k \le n$ such that: 
:$U_{\alpha_i} \subseteq U_{\alpha_k}$ for each $1 \le i \le n$. 
Then: 
:$C_i \in U_{\alpha_k}$ for each $1 \le i \le n$. 
Since $U_{\alpha_k}$ has the finite intersection property, we have: 
:$\ds \bigcap_{i \mathop = 1}^n C_i \ne \O$
Since $F \subseteq U$ was an arbitrary finite set, $U$ has the finite intersection property.
So $U$ is an upper bound for $\family {U_\alpha}_{\alpha \in A}$. 
So $\struct {S, \subseteq}$ is an ordered set such that every non-empty chain has an upper bound.
So by Zorn's Lemma $\struct {S, \subseteq}$ has a maximal element $\AA$.
Category:Tychonoff's Theorem
Tychonoff's Theorem/General Case/Proof 2/Lemma 2

== Lemma ==
Let $X$ be a set.
We say that a family $\CC$ of subsets of $X$ has the "finite intersection property" if:
:$\ds \bigcap_{S \in \SS} S \ne \O$
for all finite subsets $\SS \subseteq \CC$.
Let: 
:$\ds S = \set {\CC \subseteq \AA : \AA \text { has the finite intersection property} }$
Let $\AA$ be a $\subseteq$-maximal element of $S$ given by Lemma 1.
Let $A, B \in \AA$.
Then $A \cap B \in \AA$.
== Proof ==
Let $\set {C_1, C_2, \ldots, C_n}$ be a finite subset of $\AA$.
Then $\set {A, B, C_1, C_2, \ldots, C_n}$ is a finite subset of $\AA$.
Then since $\AA$ has the finite intersection property: 
:$\ds A \cap B \cap \bigcap_{i \mathop = 1}^n C_i = \paren {A \cap B} \cap \bigcap_{i \mathop = 1}^n C_i \in \AA$
for every finite subset $\set {C_1, C_2, \ldots, C_n}$ of $\AA$.
So $\AA \cup \set {A \cap B} \in S$ also has the finite intersection property.
Since $\AA$ is $\subseteq$-maximal in $S$, we have $\AA \cup \set {A \cap B} = \AA$. 
That is: 
:$A \cap B \in \AA$
Category:Tychonoff's Theorem
Tychonoff's Theorem/General Case/Proof 2/Lemma 3

== Lemma ==
Let $X$ be a set.
We say that a family $\CC$ of subsets of $X$ has the "finite intersection property" if:
:$\ds \bigcap_{F \in \SS} F \ne \O$
for all finite subsets $\SS \subseteq \CC$.
Let: 
:$\ds S = \set {\CC \subseteq \AA : \AA \text { has the finite intersection property} }$
Let $\AA$ be a $\subseteq$-maximal element of $S$ given by Lemma 1.
Let $A \subseteq X$ be such that: 
:$A \cap B \ne \O$
for all $B \in \AA$. 
Then $A \in \AA$. 
== Proof ==
Let $\set {C_1, \ldots, C_n}$ be a finite subset of $\AA$.
By Lemma 2, we have: 
:$\ds \bigcap_{i \mathop = 1}^n C_i \ne \O$ 
Hence, by hypothesis, we have: 
:$\ds A \cap \bigcap_{i \mathop = 1}^n C_i \ne \O$ 
So $\AA \cup \set A \in S$ has the finite intersection property.
Since $\AA$ is $\subseteq$-maximal in $S$, we have: 
:$\AA \cup \set A = \AA$
so that $A \in \AA$.
Category:Tychonoff's Theorem
Tychonoff's Theorem for Hausdorff Spaces

== Theorem ==
Let:
:$I$ be an indexing set.
Let $\family {X_i}_{i \mathop \in I}$ be an indexed family of non-empty Hausdorff spaces.
Let $\ds X = \prod_{i \mathop \in I} X_i$ be the corresponding product space.
Then $X$ is compact each $X_i$ is compact.
== Proof ==
First assume that $X$ is compact. 
From Projection from Product Topology is Continuous, the projections:
:$\pr_i : X \to X_i$ 
are continuous.
From Continuous Image of Compact Space is Compact, it follows that the $X_i$ are compact.
Assume now that each $X_i$ is compact.
By Equivalence of Definitions of Compact Topological Space it is enough to show that every ultrafilter on $X$ converges.
Thus let $\FF$ be an ultrafilter on $X$.
From Image of Ultrafilter is Ultrafilter, for each $i \in I$, the image filter $\map {\pr_i} \FF$ is an ultrafilter on $X_i$.
Each $X_i$ is compact by assumption.
So by definition of compact, each $\map {\pr_i} \FF$ converges.
From Filter on Product of Hausdorff Spaces Converges iff Projections Converge, $\FF$ converges.
So, as $\FF$ was arbitrary, $X$ is compact.
However, Equivalence of Definitions of Compact Topological Space only invokes the Ultrafilter Lemma, so this theorem is safe to use when proving the Boolean Prime Ideal Theorem from the Ultrafilter Lemma.
== Also see ==
* Tychonoff's Theorem
Category:Hausdorff Spaces
Category:Tychonoff's Theorem
Tychonoff Space is Preserved under Homeomorphism

== Theorem ==
Let $T_A = \struct {S_A, \tau_A}$ and $T_B = \struct {S_B, \tau_B}$ be topological spaces.
Let $\phi: T_A \to T_B$ be a homeomorphism.
If $T_A$ is a Tychonoff (completely regular) space, then so is $T_B$.
== Proof ==
Recall that $\struct {S, \tau}$ is a Tychonoff space :
:$\struct {S, \tau}$ is a $T_{3 \frac 1 2}$ space
:$\struct {S, \tau}$ is a $T_0$ (Kolmogorov) space.
From $T_{3 \frac 1 2}$ Space is Preserved under Homeomorphism:
:If $T_A$ is a $T_{3 \frac 1 2}$ space, then so is $T_B$.
From $T_0$ (Kolmogorov) Space is Preserved under Homeomorphism:
:If $T_A$ is a $T_0$ (Kolmogorov) space, then so is $T_B$.
Hence the result.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $2$: Separation Axioms: Functions, Products, and Subspaces
Category:Homeomorphisms (Topological Spaces)
Category:Tychonoff Spaces
Tychonoff Space is Regular, T2 and T1

== Theorem ==
Let $\struct {S, \tau}$ be a Tychonoff space.
Then $\struct {S, \tau}$ is also:
:a regular space
:a $T_2$ (Hausdorff) space
:a $T_1$ (Fréchet) space.
== Proof ==
Let $T = \struct {S, \tau}$ be a Tychonoff space.
From the definition of Tychonoff space:
:$\struct {S, \tau}$ is a $T_{3 \frac 1 2}$ space
:$\struct {S, \tau}$ is a $T_0$ (Kolmogorov) space.
We have that a $T_{3 \frac 1 2}$ space is a $T_3$ space.
From the definition, a regular space is:
:a $T_3$ space
:a $T_0$ (Kolmogorov) space.
So a Tychonoff space is a regular space.
Then we have a regular space is a $T_2$ (Hausdorff) space.
Then we have a $T_2$ (Hausdorff) space is a $T_1$ (Fréchet) space.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $2$: Separation Axioms: Completely Regular Spaces
Category:Tychonoff Spaces
Category:Regular Spaces
Category:Hausdorff Spaces
Category:T1 Spaces
Tychonoff Space is Urysohn Space

== Theorem ==
Let $\struct {S, \tau}$ be a Tychonoff space.
Then $\struct {S, \tau}$ is also an Urysohn space.
== Proof ==
Let $T = \struct {S, \tau}$ be a Tychonoff space.
Let $x, y \in S: x \ne y$.
From the definition of Tychonoff space:
:$\struct {S, \tau}$ is a $T_{3 \frac 1 2}$ space
:$\struct {S, \tau}$ is a $T_0$ (Kolmogorov) space.
From Tychonoff Space is Regular, $T_2$ and $T_1$ we use the fact that $T$ is a $T_1$ (Fréchet) space.
Clearly $\set x$ and $\set y$ are disjoint.
From the definition of $T_1$ (Fréchet) space, we have that $\set x$ and $\set y$ are closed.
So by definition of a $T_{3 \frac 1 2}$ space, there exists an Urysohn function for $\set x$ and $\set y$.
This is exactly the definition of an an Urysohn space.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $2$: Separation Axioms: Additional Separation Properties
Category:Urysohn Spaces
Category:Tychonoff Spaces
Type 1 Lever/Examples/Pliers

== Example of Type $1$ Lever ==
A pair of is an example of a type $1$ lever.
:
Its fulcrum is the hinge about which the arms rotate
The effort is the force applied by the user to the handles
The load is the reactive force applied by whatever is being gripped by the business end.
== Sources ==
* 
* 
Category:Examples of Type 1 Levers
Type 1 Lever/Examples/Scissors

== Example of Type $1$ Lever ==
A pair of is an example of a type $1$ lever.
:
Its fulcrum is the pivot.
The effort is the force applied by the user to the handles.
The load is the reactive force applied by whatever is being cut at the point of contact of the blades.
== Sources ==
* 
* 
Category:Examples of Type 1 Levers
Type 2 Lever/Examples/Nutcracker

== Example of Type $2$ Lever ==
A is an example of a type $2$ lever.
:
Its fulcrum is the pivot at which the arms meet
The effort is the force applied by the user to the handles
The load is the reaction of the nut against the arms.
== Sources ==
* 
* 
Category:Examples of Type 2 Levers
Type 2 Lever/Examples/Wheelbarrow

== Example of Type $2$ Lever ==
A is an example of a type $2$ lever.
:
Its fulcrum is the pivot at which the wheel is attached to the barrow
The effort is the force applied by the user to the handles
The load is the weight of whatever is to be carried in the barrow.
== Sources ==
* 
* 
Category:Examples of Type 2 Levers
Type 3 Lever/Examples/Foot Treadle

== Example of Type $3$ Lever ==
A on a treadle loom is an example of a type $3$ lever.
:
Its fulcrum is the pivot at which the treadle is attached to the floor
The effort is the force applied by the user to the treadle
The load is the reaction of the heddles being raised and lowered by the treadles.
== Sources ==
* 
* 
Category:Examples of Type 3 Levers
Type Space is Compact

== Theorem ==
Let $\MM$ be an $\LL$-structure.
Let $A$ be a subset of the universe of $\MM$.
The type space $\map {S_n^\MM} A$ of $n$-types over $A$ is compact.
== Proof ==
It will suffice to show that every open cover of $\map {S_n^\MM} A$ by the basic open sets $[\phi]$ of the topology has a finite subcover.
Let $\UU = \set { [\phi_i] : i \in I}$ be a cover of $\map {S_n^\MM} A$ by basic open sets.
This means that every complete $n$-type over $A$ contains some $\phi_i$.
We will find a finite subcover of $\UU$.
Let $\Gamma = \set {\neg \phi_i: i \in I}$.
Then $\map {\operatorname{Th}_\AA} M \cup \Gamma$ cannot be satisfied, since if $\NN \models \map {\operatorname{Th}_\AA} M \cup \map \Gamma {\bar b}$, then the type $\map {\operatorname{tp}_\NN} {\bar b / A}$ is a complete $n$-type in $\map {S_n^\MM} A$ which does not contain any $\phi_i$.
By the Compactness Theorem, $\map {\operatorname{Th}_\AA} M \cup \Gamma$ must have a finite subset $\Delta$ which is not satisfiable.
Since $\Delta$ is not satisfiable but $\map {\operatorname{Th}_\AA} M$ is, $\Delta$ must contain some of the $\neg \phi_i$ from $\Gamma$.
Furthermore, we must have that every model of $\map {\operatorname{Th}_\AA} M$ fails to satisfy at least one of these finitely many $\neg \phi_i$ in $\Delta$.
We claim that the finite set $\FF = \set {[\phi_i] : \neg \phi_i \in \Delta}$ is a finite subcover of $\UU$.
Since $\FF$ is clearly a subset of $\UU$, we need only show that every $p \in \map {S_n^\MM} A$ is contained in some $[\phi_i] \in \FF$.
That is, we must show that each $p \in \map {S_n^\MM} A$ contains one of these $\phi_i$.
Let $p \in \map {S_n^\MM} A$.
By definition, this means that $p \cup \map {\operatorname{Th}_\AA} M$ is satisfiable by some $\NN$.
But, as mentioned above, since $\NN \models \map {\operatorname{Th}_\AA} M$, we have that $\NN \not\models \neg \phi_i$ for some $\neg \phi_i \in \Delta$.
Since $p$ is complete, it must contain either $\phi_i$ or $\neg \phi_i$.
However, if $p$ contained $\neg \phi_i$, then $\NN \models \neg \phi_i$, which contradicts $\NN \not\models \neg \phi_i$.
Thus, $p$ contains $\phi_i$.
This demonstrates that $\FF$ is a finite subcover for $\UU$.
Thus, $\map {S_n^\MM} A$ is compact.
Category:Model Theory for Predicate Logic
UFD is GCD Domain/Proof 1

== Theorem ==
== Proof ==
Let $x \divides y$ denote $x$ divides $y$.
Let $x, y \in A$, with complete factorizations:
:$x = u x_1 \cdots x_r$
:$y = v y_1 \cdots y_s$
where:
:$u, v$ are units
:the $x_i$, $y_i$ irreducible.
We arrange the complete factorizations as follows:
:$x = u \paren {x_1 \cdots x_t} x_{t + 1} \cdots x_r$
:$y = v \paren {y_1 \cdots y_t} y_{t + 1} \cdots y_s$
where:
:$t \le \min \set {r, s}$
:For $i = 1, \ldots, t$, $x_i$ and $y_i$ are associates
:For any $i \in \set {t + 1, \ldots, r}$, $j \in \set {t + 1, \ldots, s}$, $x_i$ and $y_j$ are not associates.
Let $d = x_1 \cdots x_t$ (recall that the empty product is $1$, i.e. $d = 1$ when $t = 0$).
We claim that $d$ is a greatest common divisor for $x$ and $y$.
Certainly $d \divides x$ and $d \divides y$.
So, let $f$ be another common divisor of $x$ and $y$.
We can find $w, z \in A$ such that $x = f w$, and $y = f z$.
If $f$ is a unit, then $f \divides d$ by definition.
 $f \nmid d$.
Then the complete factorization of $f$ must contain an irreducible element that does not divide $d$.
Call this irreducible element $g$.
We have that:
:$g$ must divide some $x_j$ where $j > t$
and
:$g$ must divide some $y_k$ where $k > t$.
Either:
:$g$ is a unit, contradicting its irreducibility
or:
:$x_j$ and $y_k$ are not irreducible, which is a contradiction also.
Hence by Proof by Contradiction:
:$f \divides d$
and so $x$ and $y$ have a greatest common divisor.
Category:UFD is GCD Domain
URM Computable Functions of One Variable is Countably Infinite

== Theorem ==
The set $\mathbf U$ of all URM computable functions of $1$ variable is countably infinite.
== Proof ==
Let $\mathbf U$ be the set of all URM computable functions.
For each $f \in \mathbf U$, let $P_f$ be a URM program which computes $f$.
Such a program is very probably not unique, so in order to be definite about it, we can pick $P_f$ to be the URM program with the smallest code $\gamma \left({P_f}\right)$.
This is possible from the Well-Ordering Principle.
Let us define the function $h: \mathbf U \to \N$ as:
:$h \left({f}\right) = \gamma \left({P_f}\right)$
Since the same URM program can not compute two different functions of $1$ variable, it can be seen that $h$ is injective.
The result follows from Domain of Injection to Countable Set is Countable‎.
Category:URM Programs
Category:Countable Sets
URM Instructions are Countably Infinite

== Theorem ==
The set $\Bbb I$ of all basic URM instructions is countably infinite.
== Proof ==
We can immediately see that $\Bbb I$ is infinite as, for example, $\phi: \N \to \Bbb I$ defined as:
:$\phi \left({n}\right) = Z \left({n}\right)$
is definitely injective.
From Unique Code for URM Instruction, we see that $\beta: \Bbb I \to \N$ is also an injection.
The result follows from Domain of Injection to Countable Set is Countable.
Category:URM Programs
Category:Countable Sets
URM Programs are Countably Infinite

== Theorem ==
The set $\mathbf P$ of all URM programs is countably infinite.
== Proof ==
We can immediately see that $\mathbf P$ is infinite as the number of URM instructions is infinite.
From Unique Code for URM Program, we see that $\gamma: \mathbf P \to \N$ is also an injection.
The result follows from Domain of Injection to Countable Set is Countable.
Category:URM Programs
Category:Countable Sets
Ultraconnected Space is Connected

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space which is ultraconnected.
Then $T$ is connected.
== Proof ==
Let $T = \struct {S, \tau}$ be a topological space which is ultraconnected.
From Ultraconnected Space is Path-Connected, $T$ is path-connected.
The result follows from Path-Connected Space is Connected.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $4$: Connectedness
Category:Connected Spaces
Category:Ultraconnected Spaces
Ultraconnected Space is Path-Connected

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space which is ultraconnected.
Then $T$ is path-connected.
== Proof ==
Let $T = \struct {S, \tau}$ be ultraconnected.
Let $a, b \in S$.
Let $p \in \set a^- \cap \set b^-$ where $\set a^-$ is the closure of $\set a$.
Such a $p$ can be chosen, as $T$ being ultraconnected guarantees that $\set a^- \cap \set b^- \ne \O$.
Consider the mapping $f: \closedint 0 1 \to X$ such that:
:$\map f x = \begin{cases}
a & : x \in \hointr 0 {\dfrac 1 2} \\
p & : x = \dfrac 1 2 \\
b & : x \in \hointl {\dfrac 1 2} 1 \\
\end{cases}$
Then $f$ is continuous.
The result follows from the definition of path-connectedness.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $4$: Connectedness
Category:Path-Connected Spaces
Category:Ultraconnected Spaces
Ultraconnected Space is T4

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space which is ultraconnected.
Then $T$ is a $T_4$ space.
== Proof ==
Recall the definition of a $T_4$ space:
$T = \struct {S, \tau}$ is a $T_4$ space :
:for any two disjoint closed sets $A, B \subseteq S$, there exist disjoint open sets $U, V \in \tau$ containing $A$ and $B$ respectively.
As no two closed sets of an ultraconnected space are actually disjoint, it follows that $T_4$-ness follows vacuously.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $4$: Connectedness
Category:T4 Spaces
Category:Ultraconnected Spaces
Ultraconnected Space is not necessarily Arc-Connected

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space which is ultraconnected.
Then $T$ is not necessarily arc-connected.
== Proof ==
Let $T$ be an excluded point space.
From Excluded Point Space is Ultraconnected, $T$ is an ultraconnected space.
From Excluded Point Space is not Arc-Connected, $T$ is not arc-connected.
Hence the result.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $4$: Connectedness
Category:Ultraconnected Spaces
Category:Arc-Connected Spaces
Ultrafilter Lemma

== Theorem ==
Let $S$ be a set.
Every filter on $S$ is contained in an ultrafilter on $S$.
=== Corollary ===
== Proof using Axiom of Choice ==
== Proof using Boolean Prime Ideal Theorem ==
== Also known as ==
== Also see ==
* Boolean Prime Ideal Theorem
* Stone's Representation Theorem for Boolean Algebras
== Sources ==
Category:Ultrafilter Lemma
Category:Set Theory
Category:Filter Theory
Category:Named Theorems
Ultrafilter Lemma/Corollary

== Theorem ==
Let $S$ be a non-empty set.
Let $\AA$ be a set of subsets of $S$.
Suppose that $\AA$ has the finite intersection property.
Then there is an ultrafilter $\UU$ on $S$ such that $\AA \subseteq \UU$.
== Proof ==
Let $\II$ be the set of intersections of non-empty finite subsets of $\AA$.
Let $\FF = \set {T \in \powerset S: \exists B \in \II: B \subseteq T}$.
Note that $\AA \subseteq \II \subseteq \FF$.
$\FF$ is a filter on $S$:
Because $\AA$ has the finite intersection property:
:$\O \notin \II$
Because each element of $\FF$ is a superset of some element of $\II$:
:$\O \notin \FF$
Let $P \in \FF$ and $P \subseteq Q \subseteq S$.
Then:
:$\exists B \in \II: B \subseteq P$
and so:
: $B \subseteq Q \subseteq S$
Thus:
:$Q \in \FF$
Let $P \in \FF$ and $Q \in \FF$.
Then:
:$\exists B, C \in \II: B \subseteq P$ and $C \subseteq Q$
Then:
:$B \cap C \in \II$
and:
:$B \cap C \subseteq P \cap Q \subseteq S$
Thus:
:$P \cap Q \in \FF$
Thus, by definition, $\FF$ is a filter on $S$.
By the Ultrafilter Lemma, there exists an ultrafilter $\UU$ on $S$ such that:
:$\FF \subseteq \UU$
Because $\AA \subseteq \FF$:
:$\AA \subseteq \UU$
Category:Ultrafilter Lemma
Ultrafilter Lemma/Proof 1

== Theorem ==
== Proof ==
Let $\Omega$ be the set of filters on $S$.
From Subset Relation is Ordering, the subset relation makes $\struct {\Omega, \subseteq}$ a partially ordered set.
Let $C \subseteq \Omega$ be a non-empty chain.
Then $\bigcup C$ is again a filter on $S$.
Thus $\bigcup C$ is an upper bound of $C$.
Indeed, if $A, B \in \bigcup C$ then there there are filters $\FF, \FF' \in C$ with $A \in \FF$ and $B \in \FF'$.
We have that $C$ is a chain.
, let $\FF \subset \FF'$.
Thus $A \in \FF'$.
Hence:
:$A \cap B \in \FF'$
In particular:
:$A, B \in \bigcup C$
For any $\FF \in \Omega$ there is therefore by Zorn's Lemma a maximal element $\FF'$ such that:
:$\FF \subseteq \FF'$
The maximality of $\FF'$ is in this context equivalent to $\FF'$ being an ultrafilter.
== Also known as ==
Category:Ultrafilter Lemma
Ultrafilter Lemma/Proof 2

== Theorem ==
== Proof ==
Let $\FF$ be a filter on $S$.
Let the power set of $S$ be ordered by inclusion.
Then, by Filter on Set is Proper Filter, $\FF$ is a proper filter on $\powerset S$.
By Filter is Ideal in Dual Ordered Set, $\FF$ is an ideal in the dual of $\powerset S$.
By Singleton of Bottom is Ideal, $\set \empty$ is an ideal in $\powerset S$.
By Ideal is Filter in Dual Ordered Set, $\set \empty$ is a filter on the dual of $\powerset S$.
By the definition of Filter on Set, $\empty \notin \FF$, so $\FF$ and $\set \empty$ are disjoint.
Therefore, by the Boolean Prime Ideal Theorem, there is a prime ideal $\GG \supseteq \FF$ that is disjoint from $\set \empty$.
By Prime Ideal is Prime Filter in Dual Lattice, $\GG$ is a prime filter on the dual of the dual of $\powerset S$.
Thus, $\GG$ is a prime filter on $\powerset S$ by Dual of Dual Ordering.
But $\GG$ is disjoint from $\set \empty$, which implies that $\empty \notin \GG$.
Therefore, $\GG$ is a proper filter.
Thus, by Proper and Prime iff Ultrafilter in Boolean Lattice, $\GG$ is an ultrafilter on $\powerset S$.
But by comparing the definitions, $\GG$ is thus an ultrafilter on $S$.
== Also known as ==
Category:Ultrafilter Lemma