Characterization of T0 Space by Distinct Closures of Singletons
Theorem
Let $T = \struct {S, \tau}$ be a topological space.
Then
- $T$ is a $T_0$ space if and only if
- $\forall x, y \in S: x \ne y \implies \set x^- \ne \set y^-$
where $\set y^-$ denotes the closure of $\set y$.
Proof
Sufficient Condition
Let $T$ be a $T_0$ space.
Let $x, y \in S$ such that
- $x \ne y$
By definition of $T_0$ space:
- $\paren {\exists U \in \tau: x \in U \land y \notin U} \lor \paren {\exists U \in \tau: x \notin U \land y \in U}$
Without loss of generality, suppose
- $\exists U \in \tau: x \in U \land y \notin U$
By definition of singleton:
- $x \in \set x$
By Set is Subset of its Topological Closure:
- $\set x \subseteq \set x^-$
Then by definition of subset:
- $x \in \set x^-$
Hence by definition of intersection:
- $\set x^- \cap U \ne \O$
By definition of singleton:
- $\forall z: z \in \set y \implies z = y$
Then by definition of intersection:
- $\set y \cap U = \O$
Hence by Open Set Disjoint from Set is Disjoint from Closure
- $\set y^- \cap U = \O$
Thus:
- $\set x^- \ne \set y^-$
$\Box$
Necessary Condition
Assume that:
- $(1): \quad \forall x, y \in S: x \ne y \implies \set x^- \ne \set y^-$
By Characterization of $T_0$ Space by Closed Sets it suffices to prove that
- $\leftparen {\exists F \subseteq S: F}$ is closed $\rightparen {\land x \in F \land y \notin F}$
or
- $\leftparen {\exists F \subseteq S: F}$ is closed $\rightparen {\land x \notin F \land y \in F}$
Then assume:
- $(2): \quad \forall F \subseteq S: F$ is closed $\land x \in F \implies y \in F$
Define $F := \set y^-$
By Topological Closure is Closed:
- $F$ is closed.
We will prove now that
- $x \notin F$
Aiming for a contradiction, suppose
- $x \in F$
Then:
- $\set x \subseteq F$
By Topological Closure of Subset is Subset of Topological Closure:
- $\set x^- \subseteq F^-$
By Set is Closed iff Equals Topological Closure:
- $(3): \quad \set x^- \subseteq F$
By definition of singleton:
- $x \in \set x$
By Set is Subset of its Topological Closure:
- $\set x \subseteq \set x^-$
Then by definition of subset:
- $x \in \set x^-$
Because $\set x^-$ is closed therefore by $(2)$:
- $y \in \set x^-$
Then:
- $\set y \subseteq \set x^-$
By Topological Closure of Subset is Subset of Topological Closure:
- $F \subseteq \paren {set x^-}^-$
Then by Closure of Topological Closure equals Closure:
- $F \subseteq \set x^-$
Hence by $(3)$ and definition of set equality:
- $F = \set x^-$
This contradicts the assumption $(1)$.
Thus $x \notin F$.
By definition of singleton:
- $y \in \set y$
By Set is Subset of its Topological Closure:
- $\set y \subseteq \set y^- = F$
Thus by definition of subset:
- $y \in F$
Hence
- $\exists F \subseteq S: F$ is closed $\land x \notin F \land y \in F$
$\blacksquare$
Sources
- Mizar article TSP_1:def 5