nyuuzyou/wikis huggingface dataset:
Fort Topology is Topology

== Theorem ==
Let $T = \struct {S, \tau_p}$ be a Fort space.
Then $\tau_p$ is a topology on $T$.
== Proof ==
We have that $p \in \relcomp S \O = S$, so $\O \in \tau_p$.
We have that $\relcomp S S = \O$ which is finite, so $S \in \tau_p$.
Now consider $A, B \in \tau_p$, and let $H = A \cap B$.
If $p \notin A$ or $p \notin B$ then $p \notin A \cap B$ and so $H \in \tau_p$.
Now suppose $p \in A$ and $p \in B$.
Then:
In order for $A$ and $B$ to be open sets it follows that $\relcomp S A$ and $\relcomp S B$ are both finite.
Hence their union is also finite and so $\relcomp S H$ is finite.
So $H = A \cap B \in \tau_p$ as its complement is finite.
Now let $\UU \subseteq \tau_p$.
Then from De Morgan's Laws: Complement of Union:
:$\ds \relcomp S {\bigcup \UU} = \bigcap_{U \mathop \in \UU} \relcomp S U$
We have either of two options:
:$(1): \quad \forall U \in \UU: p \in \relcomp S U$
in which case:
:$\ds p \in \bigcap_{U \mathop \in \UU} \relcomp S U$
Or:
:$(2): \quad \exists U \in \UU: \relcomp S U$ is finite
in which case:
:$\ds \bigcap_{U \mathop \in \UU} \relcomp S U$ is finite, from Intersection is Subset.
So in either case $\ds \bigcup \UU \in \tau_p$.
== Sources ==
* : Part $\text {II}$: Counterexamples: $23 \text { - } 24$. Fort Space
Category:Fort Spaces
Fortissimo Space is Completely Normal

== Theorem ==
Let $T = \struct {S, \tau_p}$ be a Fortissimo space.
Then $T$ is a completely normal space.
Consequently, $T$ satisfies all weaker separation axioms.
== Proof ==
We have:
:Fortissimo Space is $T_1$
:Fortissimo Space is $T_5$
and so by definition $T$ is completely normal.
See Sequence of Implications of Separation Axioms for confirmation of the statement about weaker separation axioms.
== Sources ==
* : Part $\text {II}$: Counterexamples: $25$. Fortissimo Space: $1$
Category:Completely Normal Spaces
Category:Fortissimo Space
Fortissimo Space is Excluded Point Space with Countable Complement Space

== Theorem ==
Let $T = \struct {S, \tau_p}$ be a Fortissimo space.
Then $\tau_p$ is the minimal topology that is generated by the excluded point topology and the countable complement topology.
== Proof ==
Let $T_1 = \struct {S, \tau_1}$ be the excluded point space on $S$ from $p$.
Let $T_2 = \struct {S, \tau_2}$ be the countable complement space on $S$.
By definition:
:$\tau_1 = \set {H \subseteq S: p \in \relcomp S H} \cup \set S$ 
:$\tau_2 = \leftset {H \subseteq S: \relcomp S H}$ is countable $\rightset{} \cup \set \O$
By definition of Fortissimo space, we have:
:$U \in \tau_1 \implies U \in \tau_p$
:$U \in \tau_2 \implies U \in \tau_p$
So $\tau_1 \cup \tau_2 \subseteq \tau_p$.
Similarly:
:$U \in \tau_p \implies U \in \tau_1 \lor U \in \tau_2$
and so $\tau_p \subseteq \tau_1 \cup \tau_2$.
So $\tau_p = \tau_1 \cup \tau_2$ and the result follows from Union is Smallest Superset.
== Sources ==
* : Part $\text {II}$: Counterexamples: $25$. Fortissimo Space: $1$
Category:Fortissimo Space
Category:Excluded Point Topology
Category:Countable Complement Topology
Fortissimo Space is Lindelöf

== Theorem ==
Let $T = \struct {S, \tau_p}$ be a Fortissimo space.
Then $T$ is a Lindelöf space.
== Proof ==
Let $\CC$ be an open cover of $T$.
Then $\exists U \in \CC$ such that $p \in U$ and so $\relcomp S U$ is countable.
So $U$, together with an open neighborhood of each of the elements of $\relcomp S U$, is a countable subcover of $\CC$.
Hence the result by definition of Lindelöf space.
== Sources ==
* : Part $\text {II}$: Counterexamples: $25$. Fortissimo Space: $1$
Category:Lindelöf Spaces
Category:Fortissimo Space
Fortissimo Space is Paracompact

== Theorem ==
Let $T = \struct {S, \tau_p}$ be a Fortissimo space.
Then $T$ is a paracompact space.
== Proof ==
Let $\CC$ be an open cover of $T$.
Let $U_p \in \CC$ be an open set in that cover which contains $p$.
All the points of $S \setminus U_p$ are open points by definition of Fortissimo space.
Then $\DD = \set {\set s: s \in S \setminus U_p} \cup \set {U_p}$ is an open refinement of $\CC$.
Take $k \in S$:
:If $k = p$, then $U_p$ is a neighbourhood of $k$ which intersects only with $U_p$ from all the subsets in $\DD$
:If $k \ne p$, then $\set k$ is a neighbourhood of $k$ which intersects only with $\set k$ from all the subsets in $\DD$
Thus $\DD$ is by definition locally finite.
Hence, by definition, $T$ is a paracompact space.
== Sources ==
* : Part $\text {II}$: Counterexamples: $25$. Fortissimo Space: $1$
Category:Paracompact Spaces
Category:Fortissimo Space
Fortissimo Space is T1

== Theorem ==
Let $T = \struct {S, \tau_p}$ be a Fortissimo space.
Then $T$ is a $T_1$ (Fréchet) space.
== Proof ==
From Fortissimo Space is Excluded Point Space with Countable Complement Space, $T$ is an expansion of a countable complement space.
Then we have that a Countable Complement Space is $T_1$.
Then from Separation Properties Preserved by Expansion we have that as a cuntable complement space is a $T_1$ space, then so is $T$.
== Sources ==
* : Part $\text {II}$: Counterexamples: $25$. Fortissimo Space: $1$
Category:T1 Spaces
Category:Fortissimo Space
Fortissimo Space is T5

== Theorem ==
Let $T = \struct {S, \tau_p}$ be a Fortissimo space on an infinite set $S$.
Then $T$ is a $T_5$ space.
== Proof ==
Let $A, B \in \tau_p$ such that $A$ and $B$ are separated.
If $p \notin A$ and $p \notin B$ then $A$ and $B$ are both open.
Otherwise $p$ must be in exactly one of them, because if $p$ were in both they could not be separated.
, suppose $p \in A$.
Then $p \notin B$ so $B$ is open.
Now suppose $B$ were not closed.
Then $B$ is uncountable by definition of Fortissimo space.
But every open set not containing $p$ is co-countable in $S$.
So $p$ would be in $B^-$, where $B^-$ is the closure of $B$.
But then $p \in A$, by hypothesis.
So $A \cap B^- \ne \O$ and so $A$ and $B$ are not separated.
So $B$ must be closed.
Therefore $\relcomp S B$ is an open set such that $A \subseteq \relcomp S B$, and the $T_5$ separation axiom is satisfied.
== Sources ==
* : Part $\text {II}$: Counterexamples: $25$. Fortissimo Space: $1$
Category:T5 Spaces
Category:Fortissimo Space
Fortissimo Space is not Compact

== Theorem ==
Let $T = \struct {S, \tau_p}$ be a Fortissimo space.
Then $T$ is not a compact space.
== Proof ==
From the definition, $T$ is a compact space if every open cover of $T$ has a finite subcover.
Let $N \subset S$ be a countably infinite set such that $p \notin N$.
Then $\relcomp S N$ is open in $T$ by the definition of the Fortissimo space.
Let $q \in S$ such that $q \ne p$.
As $p \in \relcomp S {\set q}$ it follows that $\set q$ is open in $T$.
Then:
:$\ds S = \relcomp S N \cup \paren {\bigcup_{q \mathop \in N} \set q}$
Let $\CC$ be defined as:
:$\CC := \set {\set q: q \in N} \cup \set {\relcomp S N}$
Then from the above, $\CC$ is an open cover of $S$.
But all the sets of $\CC$ are pairwise disjoint.
Therefore $\CC$ can have no finite subcover.
Hence the space cannot be compact.
== Sources ==
* : Part $\text {II}$: Counterexamples: $25$. Fortissimo Space: $1$
Category:Fortissimo Space
Category:Compact Spaces
Fortissimo Space is not First-Countable

== Theorem ==
Let $T = \struct {S, \tau_p}$ be a Fortissimo space.
Then $T$ is not a first-countable space.
== Proof ==
This proof follows the proof from Countable Complement Space is not First-Countable.
 that $p \in S$ has a countable local basis.
That means:
:there exists a countable set of sets $\BB_p \subseteq \tau$
such that:
:$\forall B \in \BB_p: p \in B$
and such that:
:every open neighborhood of $p$ contains some $B \in \BB_p$.
So:
By definition of the fortissimo space, each of $S \setminus B$ is countable.
From Countable Union of Countable Sets is Countable it follows that $\ds \bigcup_{B \mathop \in \BB_p} \paren {S \setminus B}$ is also countable.
So $S \setminus \set p$ and therefore $S$ is also countable.
From this contradiction (as we have specified that $S$ is uncountable) it follows that our assumption that $p \in S$ has a countable local basis must be false.
Hence by definition $T$ can not be first-countable.
== Sources ==
* : Part $\text {II}$: Counterexamples: $25$. Fortissimo Space: $1$
Category:First-Countable Spaces
Category:Fortissimo Space
Fortissimo Space is not Metrizable

== Theorem ==
Let $T = \struct {S, \tau_p}$ be a Fortissimo space.
Then $\tau_p$ is not a metrizable topology.
== Proof ==
From Metric Space is First-Countable and Fortissimo Space is not First-Countable, it is deduced that $T$ is not a metrizable topology.
== Sources ==
* : Part $\text {II}$: Counterexamples: $25$. Fortissimo Space: $1$
Category:Metrizable Topologies
Category:Fortissimo Space
Fortissimo Space is not Pseudocompact

== Theorem ==
Let $T = \struct {S, \tau_p}$ be a Fortissimo space.
Then $T$ is not a pseudocompact space.
== Proof ==
Let $N_p$ be a neighborhood of $p$ such that $\relcomp S {N_p}$ is countable.
Let $\psi: \relcomp S {N_p} \to \Z_{\ne 0}$ be a bijection between $\relcomp S {N_p}$ and the non-zero integers $\Z_{\ne 0}$.
Let $\phi: S \to \set {0, 1}$ be the mapping defined as:
:$\forall x \in S: \map \phi x = \begin {cases} 0 & : x \in N_p \\ \map \psi x & : x \notin N_p \end {cases}$
Then $\phi$ is a continuous mapping.
However, $\phi$ is not bounded.
Hence the result by definition of pseudocompact space.
== Sources ==
* : Part $\text {II}$: Counterexamples: $25$. Fortissimo Space: $3$
Category:Fortissimo Space
Category:Pseudocompact Spaces
Fortissimo Space is not Separable

== Theorem ==
Let $T = \struct {S, \tau_p}$ be the fortissimo space on an uncountable set $S$.
Then $T$ is not a separable space.
== Proof ==
Let $U$ be a countable subset of $S$.
By the definition of the fortissimo space, $U$ is closed.
From Closed Set Equals its Closure, $U^- = U \ne S$.
Thus, by definition, $U$ is not everywhere dense in $T$.
Thus, there exists no countable subset of $S$ which is everywhere dense in $T$.
So, by definition, $T$ is not a separable space.
== Sources ==
* : Part $\text {II}$: Counterexamples: $25$. Fortissimo Space: $1$
Category:Separable Spaces
Category:Fortissimo Space
Fortissimo Space is not Sequentially Compact

== Theorem ==
Let $T = \struct {S, \tau_p}$ be a Fortissimo space.
Then $T$ is not sequentially compact.
== Proof ==
Let $T' = \struct {S \setminus \set p, \tau_p}$ be the subspace of $T$ induced by $S \setminus \set p$.
From Discrete Subspace of Fortissimo Space, $T'$ is a discrete topological space.
Let $H = \sequence {x_n}_{n \mathop \in \N}$ be a sequence of distinct terms of $S \setminus \set p$.
That is:
:$\forall n \in \N: x_n \ne p$
and that:
:$n \ne m \implies x_n \ne x_m$
By definition, $H$ is a sequence of distinct terms of $S \setminus \set p$.
From Convergence of Sequence in Discrete Space: Corollary, $H$ does not converge in $T'$.
$H$ is by definition countable, so from Closed Sets of Fortissimo Space it follows that $H$ is closed.
Thus by definition $S \setminus H$ is open.
Also, as $p \notin H$ by definition of $H$, it follows that $P \in S \setminus H$.
By definition, $S \setminus H$ is an open neighborhood of $p$.
Suppose $H$ converges to the limit $p$
Then, by definition of convergence, for any open set $U \in \tau_p$ such that $p \in U$, there exists some $N \in \R$ such that $n > N \implies x_n \in U$.
But $H \cap \paren {S \setminus H} = \O$, and so $H$ cannot converge to $p \in S \setminus H$.
The result follows from the fact that every subsequence of $H$ is also a sequence of distinct terms of $S \setminus \set p$.
== Sources ==
* : Part $\text {II}$: Counterexamples: $25$. Fortissimo Space: $2$
Category:Sequentially Compact Spaces
Category:Fortissimo Space
Fortissimo Space is not Sigma-Compact

== Theorem ==
Let $T = \struct {S, \tau}$ be a Fortissimo space.
Then $T$ is not a $\sigma$-compact space.
== Proof ==
From Compact Sets in Fortissimo Space we have that the only compact sets in $T$ are finite.
A union of countably many finite sets can not be an uncountable set.
Hence the result by definition of $\sigma$-compact space.
== Sources ==
* : Part $\text {II}$: Counterexamples: $25$. Fortissimo Space: $2$
Category:Fortissimo Space
Category:Sigma-Compact Spaces
Fortissimo Space is not Weakly Countably Compact

== Theorem ==
Let $T = \struct {S, \tau_p}$ be a Fortissimo space.
Then $T$ is not weakly countably compact.
== Proof ==
It suffices to show that $T$ has an infinite subset without limit points.
Consider the set $S \setminus \set p$.
Let $x \in S$.
We have:
By definition, $x$ is a limit point of $S \setminus \set p$ $\set {p, x}$ is not a neighborhood of $x$.
By definition of Fortissimo space, $\set {p, x}$ is open in $T$.
Hence it is a open neighborhood of $x$.
Therefore $x$ is not a limit point of $S \setminus \set p$.
Since $x$ is arbitrary, $S \setminus \set p$ has no limit points.
Hence $T$ is not weakly countably compact.
== Sources ==
* : Part $\text {II}$: Counterexamples: $25$. Fortissimo Space: $2$
Category:Weakly Countably Compact Spaces
Category:Fortissimo Space
Fortissimo Topology is Topology

== Theorem ==
Let $T = \struct {S, \tau_p}$ be a Fortissimo space.
Then $\tau_p$ is a topology on $T$.
== Proof ==
We have that $p \in \relcomp S \O = S$ so $\O \in \tau_p$.
We have that $\relcomp S S = \O$ so $\O \in \tau_p$.
Now consider $A, B \in \tau_p$, and let $H = A \cap B$.
If $p \notin A$ or $p \notin B$ then $p \notin A \cap B$ and so $H \in \tau_p$.
Now suppose $p \in A$ and $p \in B$.
Then:
In order for $A$ and $B$ to be open sets it follows that $\relcomp S A$ and $\relcomp S B$ are both countable.
From Countable Union of Countable Sets is Countable, their union is also countable and so $\relcomp S H$ is countable.
So $H = A \cap B \in \tau_p$ as its complement is countable.
Now let $\UU \subseteq \tau_p$.
Then:
:$\ds \relcomp S {\bigcup \UU} = \bigcap_{U \mathop \in \UU} \relcomp S U$
by De Morgan's Laws: Complement of Union.
We have either of two options:
:$(1): \quad \forall U \in \UU: p \in \relcomp S U$
in which case:
:$\ds p \in \bigcap_{U \mathop \in \UU} \relcomp S U$
Or:
:$(2): \quad \exists U \in \UU: \relcomp S U$ is countable
in which case:
:$\ds \bigcap_{U \mathop \in \UU} \relcomp S U$ is countable, from Intersection is Subset.
So in either case $\ds \bigcup \UU \in \tau_p$.
== Sources ==
* : Part $\text {II}$: Counterexamples: $25$. Fortissimo Space
Category:Fortissimo Space
Forward-Backward Induction

== Theorem ==
Let $P$ be a propositional function on the natural numbers $\N$.
Suppose that:
:$(1): \quad \forall n \in \N: \map P {2^n}$ holds.
:$(2): \quad \map P n \implies \map P {n - 1}$.
Then $\map P n$ holds for all $\forall n \in \N$.
The proof technique based on this result is called forward-backward induction.
== Proof ==
 $\exists k \in \N$ such that $\map P k$ is false.
From Power of Real Number greater than One is Unbounded Above‎:
:$\set {2^n: n \in \N}$ is unbounded above.
Therefore we can find:
:$M = 2^N > k$
Now let us create the set:
:$S = \set {n \in \N: n < M, \map P n \text { is false} }$
As $k < M$ and $\map P k$ is false:
:$S \ne \O$
As $\forall x \in S: x < M$ it follows that $S$ is bounded above.
So from Set of Integers Bounded Above by Integer has Greatest Element, $S$ has a greatest element, which we call $m$.
We have that $\map P n$ holds for $m < n \le M$.
Hence $\map P {m + 1}$ holds.
But $\map P {m + 1} \implies \map P m$.
This contradicts our assertion that $\map P n$ is false.
Hence by Proof by Contradiction there can be no such $k \in \N$ such that $\map P k$ is false.
Hence the result.
== Also known as ==
== Sources ==
* : $\S 3$: Natural Numbers: Exercise $\S 3.11 \ (5)$
Category:Forward-Backward Induction
Category:Number Theory
Category:Named Theorems
Category:Mathematical Induction
Category:Proof Techniques
Forward Difference Operator/Examples/Value of y 2

== Example of Forward Difference Operator ==
The value of $y_2$ is given by:
:$y_2 = y_0 + 2 \Delta y_0 + \Delta^2 y_0$
where:
:$\Delta y_0$ is the first forward difference of $y_0$
:$\Delta^2 y_0$ is the second forward difference of $y_0$.
== Sources ==
* 
* 
Category:Examples of Forward Difference Operator
Forward Difference Operator/Examples/Value of y k

== Example of Forward Difference Operator ==
The value of $y_k$ is given by:
:$y_k = y_0 + \ds \sum_{s \mathop = 1}^k \dbinom k s \Delta^k y_0$
where $\Delta^k y_0$ is the $k$th forward difference of $y_0$.
== Sources ==
* 
* 
Category:Examples of Forward Difference Operator
Forward Difference of Falling Factorial

== Theorem ==
Let $f: \R \to \R$ be a real function.
Let $\Delta$ denote the forward difference operator.
Let $x^{\underline m}$ be the $m$th falling factorial of $x$
Then:
:$\map \Delta {x^{\underline m} } = m x^{\underline {m - 1} }$
== Proof ==
From the definitions:
Category:Finite Calculus
Four-Line Locus

== Theorem ==
Let $4$ straight lines in the plane be given.
The problem is to find the locus of a point $P$ such that the product of the distances from $P$ to any $2$ of them is proportional to the product of the distances to the other $2$.
== Solution ==
The required locus is a conic section.
== Proof ==
== Historical Note ==
== Sources ==
* 
* 
Category:Four-Line Locus
Category:Plane Geometry
Category:Classic Problems
Four-Parts Formula

== Theorem ==
Let $\triangle ABC$ be a spherical triangle on the surface of a sphere whose center is $O$.
Let the sides $a, b, c$ of $\triangle ABC$ be measured by the angles subtended at $O$, where $a, b, c$ are opposite $A, B, C$ respectively.
We have:
:$\cos a \cos C = \sin a \cot b - \sin C \cot B$
That is:
:$\map \cos {\text {inner side} } \cdot \map \cos {\text {inner angle} } = \map \sin {\text {inner side} } \cdot \map \cot {\text {other side} } - \map \sin {\text {inner angle} } \cdot \map \cot {\text {other angle} }$
This is known as the four-parts formula, as it defines the relationship between each of four consecutive parts of $\triangle ABC$.
=== Corollary ===
== Proof ==
:
== Also see ==
* Definition:Inner Side of Spherical Triangle
* Definition:Inner Angle of Spherical Triangle
== Sources ==
* : Chapter $\text I$. Spherical Trigonometry: $8$. The four-parts formula.
Category:Spherical Trigonometry
Four-Parts Formula/Corollary

== Theorem ==
Let $\triangle ABC$ be a spherical triangle on the surface of a sphere whose center is $O$.
Let the sides $a, b, c$ of $\triangle ABC$ be measured by the angles subtended at $O$, where $a, b, c$ are opposite $A, B, C$ respectively.
Then:
:$\cos A \cos c = \sin A \cot B - \sin c \cot b$
== Proof ==
Let $\triangle A'B'C'$ be the polar triangle of $\triangle ABC$.
Let the sides $a', b', c'$ of $\triangle A'B'C'$ be opposite $A', B', C'$ respectively.
From Spherical Triangle is Polar Triangle of its Polar Triangle we have that:
:not only is $\triangle A'B'C'$ be the polar triangle of $\triangle ABC$
:but also $\triangle ABC$ is the polar triangle of $\triangle A'B'C'$.
We have:
== Sources ==
* : Chapter $\text I$. Spherical Trigonometry: $11$. Polar formulae.
Category:Analogue Formula for Spherical Law of Cosines
Four Color Theorem

== Theorem ==
Let $G$ be a planar graph.
Then $G$ can be assigned a proper vertex $k$-coloring such that $k \le 4$.
== Proof ==
== Also known as ==
== Also see ==
* Five Color Theorem
* Flawed Proofs
== Historical Note ==
== Sources ==
* 
* 
* 
* 
Category:Four Color Theorem
Category:Graph Colorings
Category:4
Category:Named Theorems
Four Color Theorem/Also known as

== Four Color Theorem: Also known as == 
In British English, the Four Color Theorem is spelled Four Colour Theorem.
Some sources hyphenate: Four-Colo(u)r Theorem.
Some sources continue to refer to it as the Four Colo(u)r problem (with or without the hyphen), acknowledging the controversial nature of its supposed proof.
== Sources ==
* 
* 
* 
* 
Category:Four Color Theorem
Four Color Theorem/Historical Note

== Historical Note on the Four Color Theorem ==
The question of the minimal number of colors that are needed to color any arbitrary planar graph was first considered by in $1852$, when he was coloring a map of the counties of England.
He conjectured that the answer was $4$.
He published this conjecture in $1878$.
In $1879$, published what he believed to be a proof, but in $1890$ it was shown by to be flawed.
In that same year, proved that $5$ colors were certainly enough.
In $1880$, another proof was published, but that was also shown to be flawed.
During the course of the century following, many developments in graph theory were made as a result of research into this problem.
, writing about it in a $1926$ publication, also drops the names of , , , , and , and cites the work of before giving a (flawed) proof of his own.
What is now believed to be a sound proof of the Four Color Theorem was presented in $1976$ by and .
Their proof relies heavily on a computer program, set up to search through all the various cases.
Hence their proof does not easily conform to 's format.
Apart from this computer-based search, the proof is similar to that of the Five Color Theorem, a related but weaker result.
Some mathematicians distrust this proof because of its reliance on computers, and its consequent inability to be checked by humans.
This is part of a broader debate in mathematics over the increasing use of computers in proofs.
== Historical Note by ==
== Sources ==
* 
* : Geometrical Problems: Various Geometrical Puzzles: $140$. -- The Four-Colour Map Theorem
* : Combinatorial & Topological Problems: Map Coloring Puzzles: $442$. The Four-Color Map Theorem
* : $4$
* : $4$
* 
* 
* 
Category:Historical Notes
Category:Four Color Theorem
Four Color Theorem for Finite Maps implies Four Color Theorem for Infinite Maps

== Theorem ==
Suppose that any finite planar graph can be assigned a proper vertex $k$-coloring such that $k \le 4$.
Then the same is true of any infinite planar graph.
== Proof ==
Let $G$ be an infinite planar graph.
Let $C$ be a set of vertices of $G$.
For each $c \in C$ let $p_c^1, p_c^2, p_c^3, p_c^4$ be propositional symbols, where
: $p_c^i$ is true the color of vertex $c$ is $i$.
Let $\PP_0$ be the vocabulary defined as:
:$\PP_0 = \set {p_c^1, p_c^2, p_c^3, p_c^4: c \in C}$
Let $\mathbf H$ be the set of all statements with the following forms:
:$(1): \quad$ $p_c^1 \lor p_c^2 \lor p_c^3 \lor p_c^4$ for each $c \in C$
:$(2): \quad$ $p_c^i \implies \neg p_c^j$ for each $c \in C$ and for each $i \ne j$
:$(3): \quad$ $\neg \paren {p_c^i \land \neg p_{c'}^i}$ for each $i$ where $c$ and $c'$ are adjacent.
Let $\MM$ be a model for $\mathbf H$ which corresponds to a proper vertex $4$-coloring of $G$.
By hypothesis, any finite planar graph can be assigned a proper vertex $4$-coloring.
Thus every finite subgraph of $G$ has a proper vertex $4$-coloring.
That is, every finite subset of $\mathbf H$ has a model.
By the Compactness Theorem for Boolean Interpretations, $\mathbf H$ has a model.
Hence the entirety of $G$ can be assigned a proper vertex $k$-coloring.
== Sources ==
* : $\S 1.11$: Compactness
* : $\text{II}.7$ First-Order Logic Semantics: Exercise $\text{II}.7.19$
Category:Graph Theory
Four Fifths as Pandigital Fraction

== Theorem ==
The fraction $\dfrac 4 5$ can be expressed as a pandigital fraction in the following interesting way:
:$\dfrac 4 5 = \dfrac {9876} {12 \, 345}$
== Proof ==
Can be found by brute force.
== Also see ==
* One Half as Pandigital Fraction
* One Third as Pandigital Fraction
* One Quarter as Pandigital Fraction
* One Fifth as Pandigital Fraction
* One Sixth as Pandigital Fraction
* One Seventh as Pandigital Fraction
* One Eighth as Pandigital Fraction
* One Ninth as Pandigital Fraction
== Historical Note ==
== Sources ==
* : $0 \cdotp 5$
* : $0 \cdotp 5$
Category:One Fifth
Category:Pandigital Fractions