T1/2 Space is T0 Space

Theorem

Let $T = \struct {S, \tau}$ be a $T_{\frac 1 2}$ topological space.

Then $T$ is $T_0$ space.

Proof

By Characterization of T0 Space by Closures of Singletons it suffices to prove that

$\forall x, y \in S: x \ne y \implies x \notin \set y^- \lor y \notin \set x^-$

where $\set y^-$ denotes the closure of $\set y$.

Let $x, y$ be points of $T$ such that:

$x \ne y$

Aiming for a contradiction, suppose:

$x \in \set y^- \land y \in \set x^-$

We will prove that:

$x \notin \set x'$

where $\set x'$ denotes the derivative of $\set x$.

Aiming for a contradiction, suppose:

$x \in \set x'$

As $S$ is open by definition of topological space by Characterization of Derivative by Open Sets:

$\exists z \in S: z \in \set x \cap S \land z \ne x$

By definition of intersection:

$z \in \set x$

This contradicts $z \ne x$ by definition of singleton.

Thus $x \notin \set x'$.

We will prove that:

$(1): \quad \lnot \forall G \in \tau: y \in G \implies \set x \cap G \ne \O$

Aiming for a contradiction, suppose:

$\forall G \in \tau: y \in G \implies \set x \cap G \ne \O$

As sublemma we will show that:

$\forall U \in \tau: y \in U \implies \exists r \in S: r \in \set x \cap U \land y \ne r$

Let $U \in \tau$ such that:

$y \in U$

Then by assumption:

$\set x \cap U \ne \O$

By definition of empty set:

$\exists z: z \in \set x \cap U$

By definition of intersection:

$z \in \set x$

Then by definition of singleton:

$z = x \ne y$

Thus:

$\exists r \in S: r \in \set x \cap U \land y \ne r$

Then by Characterization of Derivative by Open Sets:

$y \in \set x'$

By definition of relative complement:

$y \notin \relcomp S {\set x'} \land x \in \relcomp S {\set x'}$

By definition of $T_{\frac 1 2}$ space:

$\set x'$ is closed

By definition of closed set:

$\relcomp S {\set x'}$ is open

By $x \in \set y^-$ and by Condition for Point being in Closure:

$\set y \cap \relcomp S {\set x'} \ne \O$

Then by definition of empty set:

$\exists z: z \in \set y \cap \relcomp S {\set x'}$

By definition of intersection:

$z \in \set y \land z \in \relcomp S {\set x'}$

By definition of singleton:

$z = y$

Thus $z \in \relcomp S {\set x'}$ contradicts $y \notin \relcomp S {\set x'}$.

This ends the proof of $(1)$.

Then by $(1)$ and Condition for Point being in Closure:

$y \notin \set x^-$

This contradicts $y \in \set x^-$.

$\blacksquare$

Sources

• 1989: Ryszard Engelking: General Topology (revised and completed ed.)

• Mizar article TOPGEN_4:47