avewright/proofwiki-math huggingface dataset:
Theorem: Arens-Fort Space is Zero Dimensional

Let $T = \struct {S, \tau}$ denote the Arens-Fort space.
Then $T$ is zero dimensional.

Proof:
Let $q \in S$ such that $q \ne \tuple {0, 0}$.
Then from Clopen Points in Arens-Fort Space, $\set q$ is clopen.
So $\forall q \in S, q \ne \tuple {0, 0}: \set {\set q}$ is a local basis for $q$.
If we take the neighborhoods of $\tuple {0, 0}$ that are open we get that they are also closed from Neighborhood of Origin of Arens-Fort Space is Closed.
The union of the local basis forms a basis for the topology.
This basis is formed with clopen sets.
So, by definition, $T$ is a zero dimensional space.
{{qed}}
Theorem: Arens-Fort Space is Totally Separated

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

Proof:
We have that:
:The Arens-Fort Space is Zero Dimensional.
:The Arens-Fort Space is $T_0$.
Then we have that a Zero Dimensional $T_0$ Space is Totally Separated.
{{qed}}
Theorem: Isolated Points in Arens-Fort Space

Let $T = \struct {S, \tau}$ be the Arens-Fort space.
Let $q \in S: q \ne \tuple {0, 0}$.
Then $q$ is an isolated point of $T$.

Proof:
If $q \ne \tuple {0, 0}$ then from Clopen Points in Arens-Fort Space we have that $\set q$ is both closed and open in $T$.
In particular, $\set q$ is open in $T$.
The result follows from Point in Topological Space is Open iff Isolated.
{{qed}}
Theorem: Point in Topological Space is Open iff Isolated

Let $T = \left({S, \tau}\right)$ be a topological space.
Let $x \in S$.
Then $\left\{{x}\right\}$ is open in $T$ {{iff}} $x$ is an isolated point of $T$.

Proof:
Let $\left\{{x}\right\}$ be open in $T$.
Then we have that:
:$\exists \left\{{x}\right\} \in \tau: x \in \left\{{x}\right\}\subseteq S$
This is precisely the condition which ensures that $x$ is an isolated point of $T$.
Now suppose that $x$ is an isolated point of $T$.
Then by definition there exists a open set of $T$ containing no points other than $x$:
:$\exists U \in \tau: U = \left\{{x}\right\}$
That is, if $x$ is an isolated point of $T$ then $\left\{{x}\right\}$ is open in $T$.
{{qed}}
Category:Open Sets
Category:Isolated Points
luapupy565wng4ac9qxl0b6ulox69fo
Theorem: Arens-Fort Space is Scattered

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

Proof:
Let $H \subseteq T$ such that $H \ne \set {\tuple {0, 0} }$.
Then $\exists x \in H: x \ne \tuple {0, 0}$.
From Clopen Points in Arens-Fort Space, every point of $T$ apart from $\tuple {0, 0}$ is open in $T$.
So $\set x$ is an open set of $T$.
So $H \cap \set x = \set x$ and so $x$ is isolated in $H$.
Thus $H$ contains at least one point which is isolated in $H$.
On the other hand, suppose $H = \set {\tuple {0, 0} }$.
From Singleton Point is Isolated, $\tuple {0, 0}$ is an isolated point in $\set {\tuple {0, 0} } = H$.
So again $H$ contains at least one point which is isolated in $H$.
So for all $H \subseteq S$ we have that $H$ contains at least one point which is isolated in $H$.
Hence the result, by definition of scattered space.
{{qed}}
Theorem: Fortissimo Space is not Metrizable

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
:Fortissimo Space is not First-Countable
it is deduced that $\tau_p$ is not a metrizable topology.
{{qed}}
Theorem: Fortissimo Space is Paracompact

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.
{{qed}}
Theorem: Clopen Points in Modified Fort Space

Let $T = \struct {S, \tau_{a, b} }$  be a modified Fort space.
Then all points in $S \setminus \set {a, b}$ are clopen in $T$.
$a$ and $b$ themselves are not open in $T$, but they are closed in $T$.

Proof:
Let $p \in S: p \notin \set {a, b}$.
From the definition of modified Fort space, any subset of $S \setminus \set {a, b}$ is open in $T$.
It follows directly that as $p \in S \setminus \set {a, b}$ we have that $\set p \subseteq S \setminus \set {a, b}$.
Hence $p$ is open in $T$.
As for $a$ and $b$, we have that $S \setminus \set a$ and $S \setminus \set b$ are not finite and so $a$ and $b$ are not open in $T$.
{{qed|lemma}}
For all points $p \in S$ (including $a$ and $b$), we have that $\set p$ is (trivially) finite.
It follows that while $S \setminus \set p$ contains either $a$ or $b$, it is cofinite.
Thus $S \setminus \set p$ is open in $T$.
It follows by definition that $p$ is closed in $T$.
{{qed}}
Theorem: Modified Fort Space is Compact

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

Proof:
Let $\CC$ be an open cover of $T$.
Then $\exists U \in \CC: a \in U$.
Then by definition of modified Fort space, $U$ is cofinite.
That is, $S \setminus U$ is finite.
Then $S \setminus U$ is covered by a finite subcover of $\CC$.
Hence, by definition, $T$ is compact.
{{qed}}
Theorem: Modified Fort Space is T1

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

Proof:
Let $p, q \in S: p \ne q$.
There are two options:
{{begin-itemize}}
{{item|(1):|At least one of $p$ and $q$ is not in $\set {a, b}$}}
{{item|(2):|Both $p$ and $q$ are in $\set {a, b}$.}}
{{end-itemize}}
;Proof by Cases
{{begin-itemize}}
{{item|(1):|First let $p \notin \set {a, b}$ or $q \notin \set {a, b}$.
{{WLOG}}, let $p \notin \set {a, b}$.
From Clopen Points in Modified Fort Space both $\set p \in \tau_{a, b}$ and $S \setminus \set p \in \tau_{a, b}$.
So:
:$p \in \set p, q \notin \set p$
:$p \notin S \setminus \set p, q \in S \setminus \set p$
Similarly for $q \notin \set {a, b}$.
{{qed|lemma}}
}}
{{item|(2):|Next, let $p, q \in \set {a, b}$.
Let $V_p \subseteq S$ such that $p \in V_p, q \notin V_p$ and $V_p$ is finite.
Then $S \setminus V_p$ is open in $T$ containing $q$ but not $p$.
Similarly, let $V_q \subseteq S$ such that $q \in V_q, p \notin V_q$ and $V_q$ is finite.
Then $S \setminus V_q$ is open in $T$ containing $p$ but not $q$.
{{qed|lemma}}
}}
{{end-itemize}}
Hence it can be seen that $T$ is a $T_1$ space.
{{qed}}
Theorem: Modified Fort Space is not T2

Let $T = \struct {S, \tau_{a, b} }$ be a modified Fort space.
Then $T$ is not a $T_2$ (Hausdorff) space.

Proof:
Consider $U, V \in \tau_{a, b}$ such that $a \in U, b \in V$.
We have that both $U$ and $V$ are cofinite.
So $U$ and $V$ must be infinite.
Suppose $U \cap V = \O$.
Then from Intersection with Complement is Empty iff Subset it follows that $U \subseteq \relcomp S V$ and so $U$ is finite.
But this contradicts the fact that $U$ is infinite.
So $U \cap V \ne \O$.
Hence the result by definition of $T_2$ space.
{{qed}}
Theorem: Basis for Euclidean Topology on Real Number Line

Let $\R$ be the set of real numbers.
Let $\BB$ be the set of subsets of $\R$ defined as:
:$\BB = \set {\openint a b: a, b \in \R}$
That is, $\BB$ is the set of all open real intervals of $\R$:
:$\openint a b := \set {x \in \R: a < x < b}$
Then $\BB$ forms a basis for the Euclidean topology on $\R$.

Proof:
From Real Number Line is Metric Space, one can define an open interval on the set of real numbers in terms of an $\epsilon$-neighborhood.
From Open Real Interval is Open Ball, an open interval $\openint a b$ is the open $\epsilon$-ball $\map {B_\epsilon} \alpha$.
Then from Metric Induces Topology we have that:
:$\BB = \set {\openint a b: a, b \in \R}$
forms a topology on $\R$.
{{qed}}
Theorem: Real Number Line satisfies all Separation Axioms

Let $\struct {\R, \tau_d}$ be the the real number line with the usual (Euclidean) topology.
Then $\struct {\R, \tau_d}$ fulfils all separation axioms:
=== Real Number Line with Euclidean Topology is $T_0$ ===
{{:Real Number Line with Euclidean Topology is T0}}
=== Real Number Line with Euclidean Topology is $T_1$ ===
{{:Real Number Line with Euclidean Topology is T1}}
=== Real Number Line with Euclidean Topology is $T_2$ ===
{{:Real Number Line with Euclidean Topology is T2}}
=== Real Number Line with Euclidean Topology is Semiregular ===
{{:Real Number Line with Euclidean Topology is Semiregular}}
=== Real Number Line with Euclidean Topology is $T_{2 \frac 1 2}$ ===
{{:Real Number Line with Euclidean Topology is T2.5}}
=== Real Number Line with Euclidean Topology is $T_3$ ===
{{:Real Number Line with Euclidean Topology is T3}}
=== Real Number Line with Euclidean Topology is Regular ===
{{:Real Number Line with Euclidean Topology is Regular}}
=== Real Number Line with Euclidean Topology is Urysohn ===
{{:Real Number Line with Euclidean Topology is Urysohn}}
=== Real Number Line with Euclidean Topology is $T_{3 \frac 1 2}$  ===
{{:Real Number Line with Euclidean Topology is T3.5}}
=== Real Number Line with Euclidean Topology is Completely Regular ===
{{:Real Number Line with Euclidean Topology is Completely Regular}}
=== Real Number Line with Euclidean Topology is $T_4$ ===
{{:Real Number Line with Euclidean Topology is T4}}
=== Real Number Line with Euclidean Topology is Normal ===
{{:Real Number Line with Euclidean Topology is Normal}}
=== Real Number Line with Euclidean Topology is $T_5$ ===
{{:Real Number Line with Euclidean Topology is T5}}
=== Real Number Line with Euclidean Topology is Completely Normal ===
{{:Real Number Line with Euclidean Topology is Completely Normal}}
=== Real Number Line with Euclidean Topology is Perfectly $T_4$ ===
{{:Real Number Line with Euclidean Topology is Perfectly T4}}
=== Real Number Line with Euclidean Topology is Perfectly Normal ===
{{:Real Number Line with Euclidean Topology is Perfectly Normal}}
=== Real Number Line with Euclidean Topology is Fully $T_4$ ===
{{:Real Number Line with Euclidean Topology is Fully T4}}
=== Real Number Line with Euclidean Topology is Fully Normal ===
{{:Real Number Line with Euclidean Topology is Fully Normal}}

Proof:
* Real Number Line is Metric Space
* Metric Space fulfils all Separation Axioms
{{qed}}
Theorem: Real Number Line is Non-Meager

Let $\struct {\R, \tau_d}$ be the real number line with the usual (Euclidean) topology.
Then $\struct {\R, \tau_d}$ is non-meager.

Proof:
We have that the Real Number Line is Complete Metric Space.
From the Baire Category Theorem, a complete metric space is also a Baire space.
The result follows from Baire Space is Non-Meager.
{{qed}}
{{ADC|Baire Category Theorem|3}}
Theorem: Real Number Line is Non-Meager

Let $\struct {\R, \tau_d}$ be the real number line with the usual (Euclidean) topology.
Then $\struct {\R, \tau_d}$ is non-meager.

Proof:
This proof does not use the {{Axiom-link|Dependent Choice}}, as it uses intrinsic properties of the real numbers that do not necessarily hold for the general complete metric space.
{{ProofWanted}}
Theorem: Baire Space iff Open Sets are Non-Meager

Let $T = \struct {S, \tau}$ be a topological space.
Then $T$ is a Baire space {{iff}} every non-empty open set of $T$ is non-meager in $T$.

Proof:
We prove the contrapositive:
:$T$ is not a Baire space {{iff}} there exists a non-empty open set of $T$ which is meager in $T$.
We have by definition of Baire space:
:$T$ is a Baire space {{iff}} the interior of the union of any countable set of closed sets of $T$ which are nowhere dense is empty.
Therefore:
:$T$ is not a Baire space {{iff}} the interior of the union of some countable set of closed sets of $T$ which are nowhere dense is non-empty.
We have by definition of meager:
:$A$ is meager in $T$ {{iff}} it is a countable union of subsets of $S$ which are nowhere dense in $T$.
Here $I$ denotes a countable indexing set.
Theorem: Extension Realizing All Types

Let $\MM$ be an $\LL$-structure.
Let $M$ be its universe.
There is an elementary extension $\NN$ of $\MM$ such that every type over $M$ (relative to $\MM$) is realized in $\NN$.

Proof:
Let $\map S \MM$ denote the set containing all complete types over $M$ of every number of free variables.
Let $\kappa = \size{\map S \MM}$.
Use a bijection between $\kappa$ and $\map S \MM$ to write the elements of $\map S \MM$ as $p_\alpha$ for $\alpha < \kappa$.
For each $\alpha < \kappa$, let $N_\alpha$ be an elementary extension of $\MM$ which has an ordered tuple $\bar a_\alpha$ realizing $p_\alpha$.
Such extensions and tuples exist by Type is Realized in some Elementary Extension.
We will construct the extension claimed by the theorem as the union over a chain of elementary extensions defined using Transfinite Induction.
At each step, we use the Elementary Amalgamation Theorem to add on $N_\alpha$.
Base case $\alpha = 0$:
Let $\BB_0 = \MM$.
Note that $\BB_0$ is an elementary extension of $\MM$ by choice of $\NN_0$.
Limit ordinals $\alpha \le \kappa$:
Let $\ds \BB_\alpha = \bigcup_{\beta \mathop < \alpha} \BB_\beta$
$\BB_\alpha$ is an elementary extension of $\MM$ by Union of Elementary Chain is Elementary Extension.
Successor ordinals $\alpha + 1$ for $\alpha < \kappa$:
We have that $\BB_\alpha$ and $\NN_\alpha$ are both elementary extensions of $\MM$.
By the Elementary Amalgamation Theorem, there is:
:an elementary extension $\BB_{\alpha + 1}$ of $\BB_\alpha$
and:
:an elementary embedding $g_\alpha: \NN_\alpha \to \BB_{\alpha + 1}$ which is the identity on $M$ viewed as a subset of $\NN_\alpha$.
Note that $\map {g_\alpha} {\bar a_\alpha}$ realizes $p_\alpha$ in $\BB_{\alpha + 1}$ since $g_\alpha$ is elementary.
Thus $\BB_{\alpha + 1}$ is an elementary extension of $\MM$ which contains $\map {g_\alpha} {\bar a_\alpha}$ realizing $p_\alpha$.
Now, let $\ds \BB = \bigcup_{\alpha < \kappa} \BB_\alpha$.
$\BB$ is an elementary extension of each $\BB_\alpha$ by Union of Elementary Chain is an Elementary Extension.
In particular, $\BB$ is an elementary extension of $\BB_0 = \MM$
We have that:
:each $p_\alpha$ is realized in $\BB_{\alpha + 1}$ by the corresponding $\map {g_\alpha} {\bar a_\alpha}$
and:
:$\BB$ is an elementary extension of each $\BB_{\alpha + 1}$
Thus we have that $\map {g_\alpha} {\bar a_\alpha}$ realizes $p_\alpha$ in $\BB$.
{{qed}}
Category:Model Theory for Predicate Logic
dgzs5lk8qjg2fce8k68n6yepykx9nch
Theorem: Baire Space is Non-Meager

Let $T = \struct {S, \tau}$ be a Baire space (in the context of topology).
Then $T$ is non-meager in $T$.

Proof:
From Baire Space iff Open Sets are Non-Meager, all open sets of $T$ are non-meager in $T$.
But $T$ itself is an open set of $T$ by definition of topological space.
Hence the result.
{{qed}}
Theorem: Real Number Line is Separable

Let $\struct {\R, \tau_d}$ be the real number line with the usual (Euclidean) topology.
Then $\struct {\R, \tau_d}$ is a separable space.

Proof:
{{Recall|Separable Space|separable space}}
{{:Definition:Separable Space}}
From Rational Numbers form Subset of Real Numbers, the set of rational numbers $\Q$ forms a subset of the set of real numbers $\R$.
We have:
:Rational Numbers are Countably Infinite
:Rationals are Everywhere Dense in Topological Space of Reals
The result follows from the definition of separable space.
{{qed}}
Theorem: Real Number Line is Separable

Let $\struct {\R, \tau_d}$ be the real number line with the usual (Euclidean) topology.
Then $\struct {\R, \tau_d}$ is a separable space.

Proof:
Follows from:
:Real Number Line is Second-Countable
:Second-Countable Space is Separable
{{qed}}
Theorem: Double Pointed Space is T3 iff Factor Space is T3

Let $T_S = \struct {S, \tau_S}$ be a topological space.
Let $D = \struct {A, \set {\O, A} }$ be the indiscrete space on an arbitrary doubleton $A = \set {a, b}$.
Let $T = \struct {T_S \times D, \tau}$ be the double pointed topological space on $T_S$.
Then $T$ is a $T_3$ space {{iff}} $T_S$ is also a $T_3$ space.

Proof:
Let $S' = S \times \set {a, b}$.
Let $F' \subseteq S'$ such that $F'$ is closed in $T$.
Then there exists $F \subseteq S$ such that:
:$F' = F \times \set {a, b}$
or:
:$F' = F \times \O$ by definition of the double pointed topology.
If $F' = F \times \O$ then $F' = \O$ from Cartesian Product is Empty iff Factor is Empty, and the result is trivial.
So suppose $F' = F \times \set {a, b}$.
From Open and Closed Sets in Multiple Pointed Topology it follows that $F$ is closed in $T_S$.
Let $y' = \tuple {y, q} \in \relcomp {S'} {F'}$.
Then $y \notin F$.
{{qed|lemma}}
{{Recall|T3 Space|$T_3$ space}}
{{:Definition:T3 Space/Definition 1}}
Suppose that $T_S$ is a $T_3$ space.
Then we have:
{{begin-eqn}}
{{eqn | l = y'
      | o = \in
      | r = V \times \set {a, b}
}}
{{eqn | l = F'
      | o = \subseteq 
      | r = U \times \set {a, b}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = U \times \set {a, b} \cap V \times \set {a, b}
      | r = \O
}}
{{end-eqn}}
demonstrating that $T \times D$ is a $T_3$ space.
{{qed|lemma}}
Now suppose that $T \times D$ is a $T_3$ space.
Then:
:$\exists U', V' \subset T \times D: y' \in V'$ and $F' \subseteq U'$ such that $U' \cap V' = \O$
As $D$ is the indiscrete topology it follows that:
{{begin-eqn}}
{{eqn | l = U'
      | r = U \times \set {a, b}
}}
{{eqn | l = V'
      | r = V \times \set {a, b}
}}
{{end-eqn}}
for some $U, V \subseteq T$.
From Open and Closed Sets in Multiple Pointed Topology it follows that $U$ and $V$ are open in $T$.
As $U' \cap V' = \O$ it follows that $U \cap V = \O$.
It follows that $F$ and $y$ fulfil the conditions that make $T$ a $T_3$ space.
Hence the result.
{{qed}}
Theorem: Double Pointed Space is T4 iff Factor Space is T4

Let $T_S = \struct {S, \tau_S}$ be a topological space.
Let $D = \struct {A, \set {\O, A} }$ be the indiscrete space on an arbitrary doubleton $A = \set {a, b}$.
Let $T = \struct {T_S \times D, \tau}$ be the double pointed topological space on $T_S$.
Then $T$ is a $T_4$ space {{iff}} $T_S$ is also a $T_4$ space.

Proof:
Let $S' = S \times \set {a, b}$.
Let $H' \subseteq S'$ such that $H$ is closed in $T$.
Then $H' = H \times \set {a, b}$ or $H' = H \times \O$ by definition of the double pointed topology.
If $H' = H \times \O$ then $H' = \O$ from Cartesian Product is Empty iff Factor is Empty, and the result is trivial.
So suppose $H' = H \times \set {a, b}$.
From Open and Closed Sets in Multiple Pointed Topology it follows that $H$ is closed in $T$.
Suppose that $T_S$ is a $T_4$ space.
{{Recall|T4 Space|$T_4$ space}}
{{:Definition:T4 Space/Definition 1}}
Hence $A \times \set {a, b} \subseteq U \times \set {a, b}$ and $B \times \set {a, b} \subseteq V \times \set {a, b}$ and:
:$U \times \set {a, b} \cap V \times \set {a, b} = \O$
demonstrating that $T \times D$ is a $T_4$ space.
Now suppose that $T \times D$ is a $T_4$ space.
Then $\exists U', V' \in S': A' \subseteq U'$ and $B' \subseteq V'$ such that $U' \cap V' = \O$.
As $D$ is the indiscrete topology it follows that:
:$U' = U \times \set {a, b}$
:$V' = V \times \set {a, b}$
for some $U, V \subseteq T$.
From Open and Closed Sets in Multiple Pointed Topology it follows that $U$ and $V$ are open in $T$.
As $U' \cap V' = \O$ it follows that $U \cap V = \O$.
It follows that $A$ and $B$ fulfil the conditions that make $T$ a $T_4$ space.
Hence the result.
{{qed}}
Category:Separation Axioms on Double Pointed Topology
Category:Examples of T4 Spaces
ouoidptg2ljfh4au7nt3sf0efwmhg6r
Theorem: Double Pointed Space is T5 iff Factor Space is T5

Let $T_S = \struct {S, \tau_S}$ be a topological space.
Let $D = \struct {A, \set {\O, A} }$ be the indiscrete space on an arbitrary doubleton $A = \set {a, b}$.
Let $T = \struct {T_S \times D, \tau}$ be the double pointed topological space on $T_S$.
Then $T$ is a $T_5$ space {{iff}} $T_S$ is also a $T_5$ space.

Proof:
=== Necessary Condition ===
Suppose that $T \times D$ is a $T_5$ space.
Let $A, B \subseteq T$ be two separated sets.
First, we will show that $A \times D$ and $B \times D$ are also separated.
To this end, observe that:
{{begin-eqn}}
{{eqn | l = \paren {A \times D}^- \cap \paren {B \times D}
      | r = \paren {A^- \times D} \cap \paren {B \times D}
      | c = Closure of Subset of Double Pointed Topological Space
}}
{{eqn | r = \paren {A^- \cap B} \times D
      | c = Cartesian Product Distributes over Intersection
}}
{{eqn | r = \O \times D
      | c = $A$ and $B$ are separated
}}
{{eqn | r = \O
      | c = Cartesian Product is Empty iff Factor is Empty
}}
{{end-eqn}}
Also {{mutatis}}:
:$\paren {B \times D}^- \cap \paren {A \times D} = \O$
Thus $A \times D$ and $B \times D$ are separated.
Since $T \times D$ is assumed to be a $T_5$ space, find open sets $U, V$ such that:
:$U \cap V = \O$
:$A^- \times D \subseteq U$
:$B^- \times D \subseteq V$
By Open Sets of Double Pointed Topology, there are open sets $U', V'$ of $\tau$ such that:
:$U = U' \times D$
:$V = V' \times D$
We have, furthermore:
{{begin-eqn}}
{{eqn | l = \O
      | r = U \cap V
}}
{{eqn | r = \paren {U' \times D} \cap \paren {V' \times D}
}}
{{eqn | r = \paren {U' \cap V'} \times D
      | c = Cartesian Product Distributes over Intersection
}}
{{end-eqn}}
From Cartesian Product is Empty iff Factor is Empty, $U' \cap V' = \O$ since $D$ is non-empty.
By Cartesian Product of Subsets, we also infer:
:$A^- \subseteq U'$
:$B^- \subseteq V'$
It follows that $T$ is a $T_5$ space.
{{qed|lemma}}
Theorem: Double Pointed Space is T3.5 iff Factor Space is T3.5

Let $T_S = \struct {S, \tau_S}$ be a topological space.
Let $D = \struct {A, \set {\O, A} }$ be the indiscrete space on an arbitrary doubleton $A = \set {a, b}$.
Let $T = \struct {T_S \times D, \tau}$ be the double pointed topological space on $T_S$.
Then $T$ is a $T_{3 \frac 1 2}$ space {{iff}} $T_S$ is also a $T_{3 \frac 1 2}$ space.

Proof:
{{ProofWanted}}
Category:Separation Axioms on Double Pointed Topology
Category:Examples of T3.5 Spaces
en4im77omirlmtwyexq8fo752gni9p4
Theorem: Square of Vandermonde Matrix

The square of the Vandermonde matrix of order $n$:
: $\mathbf V = \begin{bmatrix}
  x_1 & x_2 & \cdots & x_n \\
  x_1^2 & x_2^2 & \cdots & x_n^2 \\
\vdots & \vdots & \ddots & \vdots \\
  x_1^n & x_2^n & \cdots & x_n^n
\end{bmatrix}$
is symmetrical in $x_1, \ldots, x_n$.
{{questionable|The case $n {{=}} 2$ left me clueless to what could possibly be intended here; only $\mathbf {V V}^T$ is trivially seen symmetric in the $x_n$, but this can hardly be called a square}}

Proof:
{{proof wanted}}
Category:Vandermonde Matrices
5cznpmmrrl7g7g1lwc0sq7m0imj6y3t
Theorem: Open and Closed Sets in Multiple Pointed Topology

Let $T = \struct {S, \tau}$ be a topological space.
Let $A$ be a finite set whose cardinality is greater than $1$.
Let $D = \struct {A, \set {\O, A} }$ be the indiscrete space on $A$.
Let $T \times D$ be a multiple pointed topological space generated from $T$ and $D$.
Let $H \subseteq T$.
Then:
:$H \times A$ is open in $T \times D$ {{iff}} $H$ is open in $T$
:$H \times A$ is closed in $T \times D$ {{iff}} $H$ is closed in $T$
:$H \times \O$ is both open and closed in $T \times D$
Let $\O \subsetneqq H_A \subsetneqq A$, that is, let $H_A$ be a non-empty proper subset of $A$.
Then $H \times H_A$ is neither open nor closed in $T \times D$.

Proof:
By definition of multiple pointed topology, $T \times D$ is the product space of $T$ with $D$:
:$T \times D = \struct {S \times A, \tau}$
where $\tau$ is the product topology on $S \times A$.
Consider the set $H \times A$.
We have that:
:$H \times A = \pr_1^{-1} \sqbrk H$
where $\pr_1: T \times D \to T$ is the first projection from $T \times D$ to $T$.
By definition of the product topology, $\pr_1: T \times D \to T$ is a continuous mapping.
Theorem: Basis for Box Topology

Let $\family {\struct {S_i, \tau_i} }_{i \mathop \in I}$ be an $I$-indexed family of topological spaces.
Let $S$ be the cartesian product of $\family {S_i}_{i \mathop \in I}$.
That is:
:$\ds S := \prod_{i \mathop \in I} S_i$
Define:
:$\ds \BB := \set {\prod_{i \mathop \in I} U_i: \forall i \in I: U_i \in \tau_i}$
Then $\BB$ is a synthetic basis on $S$.

Proof:
Let us check the two conditions for $\BB$ to be a synthetic basis in turn.