avewright/proofwiki-math huggingface dataset:
Theorem: Closed Set in Metric Space is G-Delta

Let $M = \struct {A, d}$ be a metric space.
Let $F \subset A$ be a closed set of $M$. 
Then $F$ is a $G_\delta$ set of $A$.

Proof:
{{Recall|G-Delta Set|$G_\delta$ set}}
{{:Definition:G-Delta Set}}
Let $n \in \N$.
Let $\ds F_{\frac 1 n} = \bigcup \limits_{x \mathop \in F} \map B {x, \dfrac 1 n}$, where $\map B {x, \dfrac 1 n}$ is the open ball around $x$ with radius $\dfrac 1 n$.
$F_{\frac 1 n}$ is an open set by definition of open ball.
Also, $F_{\frac 1 n}$ contains $F$ as it is the union of open balls around every element of $F$.
$\ds F \subseteq \bigcap \limits_{n \mathop = 1}^{\infty} F_{\frac 1 n}$ because $F \subseteq F_{\frac 1 n}$ for each $n \in \N$.
Note that:
:$\ds \lim_{n \mathop \to \infty} \map B {x, \dfrac 1 n} = \set x$
so the above statement holds even in the limit.
{{explain|Which above statement? It is unclear what point is being made here.}}
Let $\ds y \in \bigcap_{n \mathop = 1}^\infty F_{\frac 1 n}$.
Let $\epsilon > 0$ be given.
There exists $n \in \N$ such that $\dfrac 1 n < \epsilon$.
As $\ds y \in \bigcap_{n \mathop = 1}^\infty F_{\frac 1 n}$, there exists $x \in F$ such that $y \in \map B {x, \dfrac 1 n}$.
Therefore:
:$\map d {x, y} < \dfrac 1 n < \epsilon$
which shows that $y$ is a limit point of $F$.
Since $F$ is closed, then $y \in F$.
Therefore:
:$\ds F \supseteq \bigcap \limits_{n \mathop = 1}^\infty F_{\frac 1 n}$
We conclude that:
:$\ds F = \bigcap \limits_{n \mathop = 1}^\infty F_{\frac 1 n}$
which is a countable intersection of open sets.
Therefore $F$ is a $G_\delta$ set by definition. 
{{qed}}
Category:G-Delta Sets
Category:Metric Spaces
ox8ar025j3fy6y5qlb90o6jit1dvbzr
Theorem: Totally Disconnected Space is Totally Pathwise Disconnected

Let $T = \struct {S, \tau}$ be a topological space which is totally disconnected.
Then $T$ is a totally pathwise disconnected space.

Proof:
Let $T = \struct {S, \tau}$ be a topological space which is totally disconnected.
Then by definition $T$ contains no non-degenerate connected sets.
{{AimForCont}} $T$ is not a totally pathwise disconnected space.
That is, there exist two points $x, y \in S$ such that there exists a path between $x$ and $y$.
That is, $x$ and $y$ are path-connected.
Thus they are in the same path component.
From Path-Connected Space is Connected, $x$ and $y$ are therefore in the same component.
But that contradicts the definition of $T$ having no non-degenerate connected sets.
Hence, by Proof by Contradiction, $T$ is a totally pathwise disconnected space.
{{qed}}
Theorem: Mean Value Theorem for Integrals

Let $f$ be a continuous real function on the closed interval $\closedint a b$.
Then there exists a real number $k \in \closedint a b$ such that:
:$\ds \int_a^b \map f x \rd x = \map f k \paren {b - a}$

Proof:
From Continuous Real Function is Darboux Integrable, $f$ is Darboux integrable on $\closedint a b$.
By the Extreme Value Theorem, there exist $m, M \in \closedint a b$ such that:
:$\ds \map f m = \min_{x \mathop \in \closedint a b} \map f x$
:$\ds \map f M = \max_{x \mathop \in \closedint a b} \map f x$
Then, from Darboux's Theorem:
:$\ds \map f m \paren {b - a} \le \int_a^b \map f x \rd x \le \map f M \paren {b - a}$ 
Dividing all terms by $\paren {b - a}$ gives:
:$\ds \map f m \le \frac 1 {b - a}\int_a^b \map f x \rd x \le \map f M$
By the Intermediate Value Theorem, there exists some $k \in \openint a b$ such that:
{{begin-eqn}}
{{eqn | l = \frac 1 {b - a} \int_a^b \map f x \rd x
      | r = \map f k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int_a^b \map f x \rd x
      | r = \map f k \paren {b - a}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Mean Value Theorem for Integrals

Let $f$ be a continuous real function on the closed interval $\closedint a b$.
Then there exists a real number $k \in \closedint a b$ such that:
:$\ds \int_a^b \map f x \rd x = \map f k \paren {b - a}$

Proof:
From Continuous Real Function is Darboux Integrable, $f$ is Darboux integrable on $\closedint a b$.
Let $F : \closedint a b \to \R$ be a real function defined by: 
:$\ds \map F x = \int_a^x \map f x \rd x$
We are assured that this function is well-defined, since $f$ is integrable on $\closedint a b$.
From Fundamental Theorem of Calculus: First Part, we have: 
: $F$ is continuous on $\closedint a b$
: $F$ is differentiable on $\openint a b$ with derivative $f$
By the Mean Value Theorem, there therefore exists $k \in \openint a b$ such that: 
:$\map {F'} k = \dfrac {\map F b - \map F a} {b - a}$
As $F$ is differentiable on $\openint a b$ with derivative $f$: 
:$\map {F'} k = \map f k$
We therefore have: 
{{begin-eqn}}
{{eqn	| l = \map f k
	| r = \frac {\map F b - \map F a} {b - a}
}}
{{eqn	| r = \frac 1 {b - a} \paren {\int_a^b \map f x \rd x - \int_a^a \map f x \rd x}
}}
{{eqn	| r = \frac 1 {b - a} \int_a^b \map f x \rd x
	| c = Definite Integral on Zero Interval
}}
{{end-eqn}}
giving: 
:$\ds \int_a^b \map f x \rd x = \paren {b - a} \map f k$
as required.
{{qed}}
Theorem: Closure in Infinite Particular Point Space is not Compact

Let $T = \struct {S, \tau_p}$ be an infinite particular point space.
Let $A \in \tau_p$ be open in $T$.
Let $A^-$ be the closure of $A$.
Then $A^-$ is not compact.

Proof:
From Closure of Open Set of Particular Point Space, we have that $A^- = S$.
The result follows from Infinite Particular Point Space is not Compact.
{{qed}}
Theorem: Cover of Doubletons of Infinite Particular Point Space has no Locally Finite Refinement

Let $T = \struct {S, \tau_p}$ be an infinite particular point space.
Let $\CC$ be the open cover of $T$ defined as:
:$\CC = \set {\set {x, p}: x \in S, x \ne p}$
Then $\CC$ has no open refinement which is locally finite.

Proof:
Suppose $T$ is an infinite particular point space.
As $S$ is infinite, $\CC$ is also infinite.
Let $x \in S, x \ne p$.
Then any neighborhood of $x$ must contain $p$, by the nature of the particular point topology.
But $p$ is contained in all elements of $\CC$.
That is:
:$\forall C \in \CC: p \in C$
So any neighborhood of $x$ intersects with all elements of the open cover $\CC$.
As $\CC$ is infinite, it therefore has no open refinement which is locally finite.
{{qed}}
Theorem: Path-Connected iff Path-Connected to Point

Let $T = \struct {S, \tau}$ be a topological space.
Let $U \subseteq S$ be a non-empty subset of $T$.
Then $U$ is path-connected {{iff}}:
:$\exists p \in U: \forall q \in U: \exists f: \closedint 0 1 \to U: f$ continuous, $\map f 0 = p$ and $\map f 1 = q$

Proof:
=== Necessary Condition ===
When $U$ is path-connected, any $p \in U$ satisfies the assertion.
Because $U$ is non-empty, such a $p$ exists.
{{qed|lemma}}
Theorem: Uncountable Fort Space is not Separable

Let $T = \struct {S, \tau_p}$ be a Fort space on an uncountable set $S$.
Then $T$ is not a separable space.

Proof:
Let $C \subseteq S$ be a countable set.
Since $S$ is uncountable, by Uncountable Set less Countable Set is Uncountable, so is $\relcomp S C$.
Thus there exists some point $x \in \relcomp S C$ such that $x \ne p$.
By Clopen Points in Fort Space, $\set x \in \tau_p$. 
By Empty Intersection iff Subset of Complement, we have $C \cap \set x = \O$.
Therefore $C$ is not everywhere dense.
Since $C$ is arbitrary, $T$ is not a separable space.
{{qed}}
Theorem: Countable Fort Space is Separable

Let $T = \struct {S, \tau_p}$ be a Fort space on a countably infinite set $S$.
Then $T$ is a separable space.

Proof:
This result follows trivially from Countable Space is Separable.
{{qed}}
Theorem: Countable Fort Space is Second-Countable

Let $T = \struct {S, \tau_p}$ be a Fort space on a countably infinite set $S$.
Then $T$ is a second-countable space.

Proof:
From Subset of Countably Infinite Set is Countable, $S \setminus \set p$ is countable.
Let $f: \N \to S$ be an enumeration of $S \setminus \set p$.
For brevity, let us write $s_n$ for $\map f n$.
Now define, for $n \in \N$, $S_n = S \setminus \set {s_0, \ldots, s_{n - 1} }$.
Note that $s_n \ne p$ for all $n \in \N$, so that $p \in S_n$ for all $n$.
By Relative Complement of Relative Complement, $S \setminus S_n = \set {s_0, \ldots, s_{n - 1} }$ and so $S_n \in \tau_p$.
Also, define $S'_n = \set {s_n}$.
Since $s_n \ne p$, $S'_n$ is open in $\tau_p$ as well.
From Finite Union of Countable Sets is Countable, $\BB := \set {S_n : n \in \N} \cup \set {S'_n : n \in \N}$ is countable.
Let us verify that $\BB$ forms a basis for $\tau_p$.
So let $U \subseteq S$ be open in $\tau_p$.
If $p \notin U$ then $\ds U = \bigcup \set {S'_n: s_n \in U}$ because the $s_n$ form an enumeration of $S \setminus \set p$.
Now if $p \in U$, then by definition of the Fort topology, $S \setminus U$ must be finite.
It follows that $A = \set {n \in \N: s_n \in S \setminus U}$ is also finite.
From Subset of Naturals is Finite iff Bounded, there exists an $N \in \N$ such that $N - 1 > n$ for all $n \in A$.
Therefore, $A \subseteq \set {0, \ldots, N - 1}$ and hence:
:$S \setminus U \subseteq \set {s_0, \ldots, s_{N - 1} }$
From Set Complement inverts Subsets, also:
:$S_N = S \setminus \set {s_0, \ldots, s_{N - 1} } \subseteq U$
It follows that $\BB$ is a basis for $\tau_p$.
Since $\BB$ is countable, we conclude $T$ is second-countable.
{{qed}}
Theorem: Fort Space is Regular

Let $T = \struct {S, \tau_p}$ be a Fort space.
Then $T$ is a regular space.

Proof:
We have that the Fort Space is Completely Normal.
The result follows from tracing the relevant implications on Sequence of Implications of Separation Axioms.
{{qed}}
Theorem: Countable Fort Space is Metrizable

Let $T = \struct {S, \tau_p}$ be a Fort space on a countably infinite set $S$.
Then $T$ is a metrizable space.

Proof:
We have:
:Fort Space is Regular
:Countable Fort Space is Second-Countable.
The result follows from Urysohn's Metrization Theorem.
{{qed}}
Theorem: Fortissimo Space is not Compact

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.
{{qed}}
Theorem: Fortissimo Space is not Sequentially Compact

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 {{Corollary|Convergence of Sequence in Discrete Space}}, $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$.
{{qed}}
Theorem: Fortissimo Space is not Weakly Countably Compact

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:
{{begin-eqn}}
{{eqn | l = \paren {S \setminus \paren {S \setminus \set p} } \cup \set x
      | r = \set p \cup \set x
      | c = 
}}
{{eqn | r = \set {p, x}
      | c = 
}}
{{end-eqn}}
By definition, $x$ is a limit point of $S \setminus \set p$ {{iff}} $\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.
{{qed}}
Theorem: Fortissimo Space is not Pseudocompact

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.
{{qed}}
Theorem: Double Pointed Fortissimo Space is Weakly Countably Compact

Let $T = \struct {S, \tau_p}$ be a Fortissimo space.
Let $T \times D$ be the double pointed topology on $T$.
Then $T \times D$ is weakly countably compact.

Proof:
Let $D = \set {0, 1}$.
Let $\tuple {p, 0}$ belong to some infinite $A \subseteq S$.
Then its twin $\tuple {p, 1}$ is a limit point of $A$.
Hence the result by definition of weakly countably compact.
{{qed}}
Theorem: Double Pointed Fortissimo Space is Lindelöf

Let $T = \struct {S, \tau}$ be a Fortissimo space.
Let $T \times D$ be the double pointed topology on $T$.
Then $T \times D$ is a Lindelöf space.

Proof:
Let $D = \set {0, 1}$.
Let $\CC$ be an open cover of $T \times D$.
Then $\exists A \times B \in \CC$ such that $\tuple {p, 0} \in A \times B$.
We must have $\relcomp S A$ is countable and $B = D$.
Hence $\relcomp S A \times D$, a product of countable sets, must be countable.
So $A \times D$, together with an open neighborhood of each of the elements of $\relcomp S A \times D$, is a countable subcover of $\CC$.
Hence the result by definition of Lindelöf space.
{{qed}}
Theorem: Double Pointed Fortissimo Space is not Sigma-Compact

Let $T = \struct {S, \tau}$ be a Fortissimo space.
Let $T \times D$ be the double pointed topology on $T$.
Then $T \times D$ is not $\sigma$-compact.

Proof:
{{proof wanted|Use the same argument as Fortissimo Space is not Sigma-Compact}}
Theorem: Double Pointed Fortissimo Space is not Pseudocompact

Let $T = \struct {S, \tau}$ be a Fortissimo space.
Let $T \times D$ be the double pointed topology on $T$.
Then $T \times D$ is not pseudocompact.

Proof:
{{proof wanted|Use the same argument as Fortissimo Space is not Pseudocompact}}
Theorem: Arens-Fort Space is Non-Meager

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Then $T$ is a non-meager space.

Proof:
From Meager Sets in Arens-Fort Space, we have that $A \subseteq S$ is meager in $T$ {{iff}} $A = \set {\tuple {0, 0} }$.
So as $\set {\tuple{0, 0} } \ne S \subseteq S$, it follows that $T$ is non-meager.
{{qed}}
Theorem: Arens-Fort Space is not Extremally Disconnected

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Then $T$ is not extremally disconnected.

Proof:
Let $\map {S_m} V$ denote the set:
:$\map {S_m} V := \set {n: \tuple {m, n} \notin V}$
where $V \subseteq \Z_{\ge 0} \times \Z_{\ge 0}$ (the same set $S_m$ used in the definition of the Arens-Fort space).
Let $U = \set {\tuple {n, m}: \exists k: m = 2 k} \setminus \set {\tuple {0, 0} }$.
From the definition of the Arens-Fort space, $U$ is open in $T$ since $\left({0, 0}\right) \notin U$.
We have that:
:$\tuple {0, 0} \in \relcomp S U$
and:
:$\map {S_m} U$ is infinite for any $m \in \N$.
Thus by definition of the Arens-Fort space, $\relcomp S U$ is not open in $T$.
So $U$ is not closed in $T$.
Let $U^-$ denote the closure of $U$.
We have that:
:$\tuple {0, 0} \notin \relcomp S {U \cup \set {\tuple {0, 0} } }$
Therefore by definition of the Arens-Fort space, $\relcomp S {U \cup \set {\tuple {0, 0} } }$ is open in $T$.
Therefore $U \cup \set {\tuple {0, 0} }$ is closed in $T$.
From Set Closure is Smallest Closed Set in Topological Space, it follows that $U^- = U \cup \set {\tuple {0, 0} }$.
We have that:
:$\tuple {0, 0} \in U \cup \set {\tuple {0, 0} }$
and:
:$\map {S_m} {U \cup \set {\tuple {0, 0} } }$ is infinite for any $m \in \N$.
Therefore by definition of the Arens-Fort space, $U \cup \set {\tuple {0, 0} }$ is not open.
Thus we have created an open set $U$ whose closure $U^-$ is not itself open.
Thus by definition the  Arens-Fort space is not extremally disconnected.
{{qed}}
Theorem: Modified Fort Space is Totally Disconnected

Let $T = \struct {S, \tau_{a, b} }$ be a modified Fort space.
Then $T$ is totally disconnected.

Proof:
We have:
:Modified Fort Space is Scattered
:Modified Fort Space is $T_1$
We also have:
:Scattered $T_1$ Space is Totally Disconnected
Hence the result.
{{qed}}
Theorem: Modified Fort Space is not Locally Connected

Let $T = \struct {S, \tau_{a, b} }$ be a modified Fort space.
Then $T$ is not locally connected.

Proof:
We have:
:Modified Fort Space is Totally Disconnected
:Totally Disconnected and Locally Connected Space is Discrete
We also have:
:Modified Fort Space is not $T_2$
:Discrete Space satisfies all Separation Properties
Hence modified Fort space is not the discrete space, and the result follows.
{{qed}}
Theorem: Sets in Modified Fort Space are Disconnected

Let $T = \struct {S, \tau_{a, b}}$ be a modified Fort space.
Let $H$ be a subset of $S$ with more than one point.
Then $H$ is disconnected.

Proof:
By Isolated Points in Subsets of Modified Fort Space:
:$\exists x \in H: x$ is isolated
By Point in Topological Space is Open iff Isolated, $\set x$ is open in $T$.
By Modified Fort Space is $T_1$ and definition of $T_1$ space, $\set x$ is closed in $T$.
Therefore $\relcomp S {\set x}$ is open in $T$.
Then we have:
{{begin-eqn}}
{{eqn | l = H
      | o = \subseteq
      | r = S
}}
{{eqn | r = \set x \cup \relcomp S {\set x}
      | c = Union with Relative Complement
}}
{{eqn | l = H \cap \set x \cap \relcomp S {\set x}
      | o = \subseteq
      | r = \set x \cap \relcomp S {\set x}
      | c = Intersection is Subset
}}
{{eqn | r = \O
      | c = Intersection with Relative Complement is Empty
}}
{{eqn | ll = \leadsto
      | l = H \cap \set x \cap \relcomp S {\set x}
      | r = \O
      | c = Subset of Empty Set
}}
{{eqn | l = H \cap \set x
      | r = \set x
}}
{{eqn | o = \ne
      | r = \O
}}
{{eqn | l = H \cap \relcomp S {\set x}
      | r = H \setminus \set x
      | c = Set Difference as Intersection with Relative Complement
}}
{{eqn | o = \ne
      | r = \O
      | c = $H$ has more than one point
}}
{{end-eqn}}
This shows that $H$ is disconnected.
{{qed}}
Theorem: Clopen Sets in Modified Fort Space

Let $T = \struct {S, \tau_{a, b} }$ be a modified Fort space.
Let $H \subseteq S$ be clopen in $T$.
If $a \in H$, then $b \in H$ as well.
That is, any clopen set of $T$ must contain '''both''' or '''neither''' of $a$ and $b$.

Proof:
Let $A$ be both closed and open in $T$.
Let $S = A \mid B$ be a separation of $S$ into the open sets $A$ and $B$.
Then by definition $B$ is also both closed and open in $T$.
Let $a \in A$.
Suppose $b \in B$.
As $A$ is open it must contain all but a finite number of points of $S$.
Thus $A$ must itself be infinite.
But then $B$ can not be open, as $b \in B$ and there is more than a finite number of points in $A$.
So if $a \in A$ then $b \in A$ as well.
{{qed}}
Theorem: Modified Fort Space is not Totally Separated

Let $T = \struct {S, \tau_{a, b} }$ be a modified Fort space.
Then $T$ is not totally separated.

Proof:
We have:
:Totally Separated Space is $T_{2 \frac 1 2}$
But we have:
:Modified Fort Space is not $T_{2 \frac 1 2}$
The result follows from Modus Tollendo Tollens.
{{qed}}
Theorem: Modified Fort Space is not Zero Dimensional

Let $T = \struct {S, \tau_{a, b} }$ be a modified Fort space.
Then $T$ is not zero dimensional.

Proof:
We have Modified Fort Space is not $T_3$.
We also have Zero Dimensional Space is $T_3$.
The result follows by Modus Tollendo Tollens.
{{qed}}
Theorem: Modified Fort Space is Scattered

Let $T = \struct {S, \tau_{a, b} }$ be a modified Fort space.
Then $T$ is scattered.

Proof:
We have that a modified Fort space is $T_1$.
We also have that a dense-in-itself subset of a $T_1$ space is infinite.
But from Isolated Points in Subsets of Modified Fort Space, we have that any subset of $T$ with more than two points has at least one isolated point.
So any dense-in-itself subset of $T$ must have an isolated point.
Hence the result, by definition of scattered space.
{{qed}}
Theorem: Isolated Points in Subsets of Modified Fort Space

Let $T = \struct {S, \tau_{a, b} }$ be a modified Fort space.
Let $H \subseteq S$ contain more than two points.
Then $H$ contains an isolated point.

Proof:
Let $H \subseteq S$ contain more than two points.
From {{Defof|Modified Fort Space}}, we can write:
:$S = N \cup \set a \cup \set b$
where $N$ is an infinite set.
Suppose $H \cap N \ne \O$.
Let $x \in H \cap N$.
Then:
:$\set x \subset N$
Therefore:
:$\set x \in \tau_{a, b}$
This shows that $x$ is isolated.
Suppose $H \cap N = \O$.
By Empty Intersection iff Subset of Complement:
:$H \subseteq \relcomp S N = \set {a, b}$
Because $H$ contains at least $2$ elements:
:$H = \set {a, b}$
Because $a \in \relcomp S {\set b}$ and $\relcomp S {\relcomp S {\set b} } = \set b$ is a finite set:
:$\relcomp S {\set b} \in \tau_{a, b}$
Thus:
:$H \cap \relcomp S {\set b} = \set a$
This shows that $a$ is isolated.
Therefore $H$ must contain an isolated point.
{{qed}}
Theorem: Modified Fort Space is Sequentially Compact

Let $T = \struct {S, \tau_{a, b} }$ be a modified Fort space.
Then $T$ is sequentially compact.

Proof:
Let $\sequence {x_n}_{n \mathop \in \N}$ be an infinite sequence in $T$.
Suppose $\sequence {x_n}$ takes an infinite number of distinct values in $S$.
Then there is an infinite subsequence $\sequence {x_{n_r} }_{r \mathop \in \N}$ with distinct terms.
Let $U$ be a neighborhood of $a$.
Then $S \setminus U$ is a finite set by definition.
Thus there exists $N \in \N$ such that $\forall r > N: x_{n_r} \in U$.
Thus $\sequence {x_{n_r} }$ converges to $a$.
Otherwise $\sequence {x_n}$ only takes a finite number of distinct values.
Then, since $\sequence {x_n}$ is infinite, there exists $x \in S$ such that:
:$\forall N \in \N: \exists n > N: x = x_n$
This implies that we can take a subsequence of $\sequence {x_n}$ which is constant, and which converges to that constant.
We can conclude then that, by definition, $T$ is a sequentially compact space.
{{qed}}
Theorem: Tangent Function is Odd

:$\map \tan {-x} = -\tan x$
That is, the tangent function is odd.

Proof:
{{begin-eqn}}
{{eqn | l = \map \tan {-x}
      | r = \frac {\map \sin {-x} } {\map \cos {-x} }
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \frac {-\sin x} {\cos x}
      | c = Sine Function is Odd; Cosine Function is Even
}}
{{eqn | r = -\tan x
      | c = Tangent is Sine divided by Cosine
}}
{{end-eqn}}
{{qed}}