Equivalence of Definitions of T3 Space

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
=== Definition by Open Sets ===
=== Definition by Closed Neighborhoods ===
=== Definition by Intersection of Closed Neighborhoods ===
== Proof ==
=== Definition by Open Sets implies Definition by Closed Neighborhoods ===
Let $T = \struct {S, \tau}$ be a topological space for which:
:$\forall F \subseteq S: \relcomp S F \in \tau, y \in \relcomp S F: \exists U, V \in \tau: F \subseteq U, y \in V: U \cap V = \O$ 
Let $U \in \tau$, and let $x \in U$.
Then by Relative Complement of Relative Complement:
:$\relcomp S {\relcomp S U} \in \tau$
So by definition of closed:
:$\relcomp S U$ is closed
and:
:$x \notin \relcomp S U$
We have by hypothesis:
:$\exists A, B \in \tau: \relcomp S U \subseteq A, x \in B: A \cap B = \O$ 
It follows that:
That is:
:$x \in \relcomp S A \subseteq U$
So we have demonstrated that there exists a closed neighborhood $\relcomp S A$ of $x$ contained in $U$.
As $U, x$ are arbitrary:
:$\forall U \in \tau: \forall x \in U: \exists N_x: \relcomp S {N_x} \in \tau: \exists V \in \tau: x \in V \subseteq N_x \subseteq U$
=== Definition by Closed Neighborhoods implies Definition by Intersection of Closed Neighborhoods ===
Let $T = \struct {S, \tau}$ be a topological space for which:
:$\forall U \in \tau: \forall x \in U: \exists N_x: \relcomp S {N_x} \in \tau: \exists V \in \tau: x \in V \subseteq N_x \subseteq U$
where $N_x$ denotes a neighborhood of $x$.
Let $H \subseteq S$ such that:
:$\relcomp S H \in \tau$
Let $C_H$ be the set of all closed neighborhoods of $H$:
:$C_H = \set {N_H: \relcomp S {N_H} \in \tau, \exists V \in \tau: H \subseteq V \subseteq N_H}$
By construction:
:$H \subseteq \bigcap C_H$
Let:
:$x \notin H$
Then:
:$x \in \relcomp S H \in \tau$
We have by hypothesis:
:$\exists N_x: \relcomp S {N_x} \in \tau: \exists V \in \tau: x \in V \subseteq N_x \subseteq \relcomp S H$
It follows that:
Therefore by construction of $C_H$:
:$\relcomp S V \in C_H$
Then:
That is:
We have shown that:
:$\bigcap C_H \subseteq H$
and:
:$H \subseteq \bigcap C_H$
So by definition of set equality:
:$\bigcap C_H = H$
As $H$ is arbitrary:
:$\forall H \subseteq S: \relcomp S H \in \tau: H = \bigcap \set {N_H: \relcomp S {N_H} \in \tau, \exists V \in \tau: H \subseteq V \subseteq N_H}$
=== Definition by Intersection of Closed Neighborhoods implies Definition by Open Sets ===
Let $T = \struct {S, \tau}$ be a topological space for which:
:$\forall H \subseteq S: \relcomp S H \in \tau: H = \bigcap \set {N_H: \relcomp S {N_H} \in \tau, \exists V \in \tau: H \subseteq V \subseteq N_H}$
Let $F \subseteq S$ and $\relcomp S F \in \tau$.
We have by hypothesis:
:$F = \bigcap \set {N_F: \relcomp S {N_F} \in \tau, \exists V \in \tau: F \subseteq V \subseteq N_F}$
Pick arbitrary $x \notin F$. 
Then:
:$\exists N \subseteq S: \relcomp S N \in \tau, \exists V \in \tau: F \subseteq V \subseteq N$
Because $x \notin F \subseteq N$:
:$x \in \relcomp S N$
Because $V \subseteq N$, it follows from Empty Intersection iff Subset of Complement that:
:$V \cap \relcomp S N = \O$
Therefore we have:
As $F$ and $x$ are arbitrary:
:$\forall F \subseteq S: \relcomp S F \in \tau, y \in \relcomp S F: \exists U, V \in \tau: F \subseteq U, y \in V: U \cap V = \O$ 
== Sources ==
* : Part $\text I$: Basic Definitions: Section $2$: Separation Axioms
* : Problems: $\S 2: \ 9$
Category:T3 Spaces