Topology Defined by Neighborhood System
Theorem
Let $S$ be a set.
Let $\family {\NN_x}_{x \mathop \in S}$ be an indexed family where $\NN_x$ is non-empty set of subsets of $S$.
Assume that
- $(\text N 1): \quad \forall x \in S, U \in \NN_x: x \in U$
- $(\text N 2): \quad \forall x \in S, U \in \NN_x, y \in U:\exists V \in \NN_y: V \subseteq U$
- $(\text N 3): \quad \forall x \in S, U_1, U_2 \in \NN_x: \exists U \in \NN_x: U \subseteq U_1 \cap U_2$
Then $T = \struct {S, \tau}$ is a topological space where:
- $\ds \tau = \set {\bigcup \GG: \GG \subseteq \bigcup_{x \mathop \in S} \NN_x}$
Moreover, $\family {\NN_x}_{x \mathop \in S}$ is a neighborhood system of $T$.
Proof
Define:
- $\BB := \ds \bigcup_{x \mathop \in S} \NN_x$
According to Topology Defined by Basis it should be proved that
- $(\text B 1): \quad \forall A_1, A_2 \in \BB: \forall x \in A_1 \cap A_2: \exists A \in \BB: x \in A \subseteq A_1 \cap A_2$
- $(\text B 2): \quad \forall x \in S: \exists A \in \BB: x \in A$
Ad $(\text B 1)$:
Let $A_1, A_2 \in \BB$.
Let $x \in A_1 \cap A_2$.
By definition of intersection:
- $x \in A_1 \land x \in A_2$
By definition of union:
- $\exists x_1 \in S: A_1 \in \NN_{x_1}$
and
- $\exists x_2 \in S: A_2 \in \NN_{x_2}$
By $(\text N 2)$:
- $\exists V_1 \in \NN_x: V_1 \subseteq A_1$
and
- $\exists V_2 \in \NN_x: V_2 \subseteq A_2$
By $(\text N 3)$:
- $\exists U \in \NN_x: U \subseteq V_1 \cap V_2$
By definition of union:
- $U \in \BB$
By Set Intersection Preserves Subsets:
- $V_1 \cap V_2 \subseteq A_1 \cap A_2$
Thus by Subset Relation is Transitive:
- $U \subseteq A_1 \cap A_2$
Ad $(\text B 2)$:
Let $x \in S$.
By definition of empty set:
- $\exists U: U \in \NN_x$
By $(\text N 1)$:
- $x \in U$
By definition of union:
- $U \in \BB$
Thus:
- $\exists A \in \BB: x \in A$
By definition of $\tau$ and $\BB$:
- $\tau = \set {\bigcup \GG: \GG \subseteq \BB}$
Thus by Topology Defined by Basis:
- $T = \struct {S, \tau}$ is a topological space
It remains to prove that
- $\family {\NN_x}_{x \mathop \in S}$ is a neighborhood system
Let $x \in S$.
Let $U \in \tau$.
By definition of $\tau$:
- $\exists \GG \subseteq \BB: U = \bigcup \GG$
Let $x \in U$.
By definition of union:
- $\exists V \in \GG: x \in V$
By definition of subset:
- $V \in \BB$
By definition of union:
- $\exists y \in S: V \in \NN_y$
By $(\text N 2)$:
- $\exists W \in \NN_x: W \subseteq V$
By Set is Subset of Union/Set of Sets:
- $V \subseteq U$
Thus by Subset Relation is Transitive:
- $\exists W \in \NN_x: W \subseteq U$
Thus by definition:
- $\NN_x$ is a local basis.
$\blacksquare$
Sources
- Mizar article TOPGEN_3:3