Topology Defined by Basis
Theorem
Let $S$ be a set.
Let $\BB$ be a set of subsets of $S$.
Suppose that
- $(\text B1): \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 B2): \quad \forall x \in X: \exists A \in \BB: x \in A$
- $\tau = \set {\bigcup \GG: \GG \subseteq \BB}$
Then:
- $T = \struct {S, \tau}$ is a topological space
- $\BB$ is a basis of $T$.
Proof
We have to prove Open Set Axioms:
Open Set Axiom $\paren {\text O 1 }$: Union of Open Sets
Let $\FF \subseteq \tau$.
Define by definition of $\tau$ a family $\family {\GG_A}_{A \mathop \in \FF}$ such that
- $\forall A \in \FF: A = \bigcup \GG_A \land \GG_A \subseteq \BB$.
By General Self-Distributivity of Set Union:
- $\ds \bigcup \bigcup_{A \mathop \in \FF} \GG_A = \bigcup_{A \mathop \in \FF} \bigcup \GG_A = \bigcup \FF$
By Union of Family of Subsets is Subset:
- $\ds \bigcup_{A \mathop \in \FF} \GG_A \subseteq \BB$
Thus by definition of $\tau$
- $\bigcup \FF \in \tau$
$\Box$
Open Set Axiom $\paren {\text O 2 }$: Pairwise Intersection of Open Sets
Let $A$ and $B$ be elements of $\tau$.
By definition of $\tau$ there exist subsets $\GG_A$ and $\GG_B$ of $\BB$ such that:
- $A = \bigcup \GG_A$ and $B = \bigcup \GG_B$ and $\GG_A, \GG_B \subseteq \BB$
Set $\GG_C = \set {C \in \BB: C \subseteq A \cap B}$
By Union of Subsets is Subset:
- $\bigcup \GG_C \subseteq A \cap B$
We will prove the inclusion: $A \cap B \subseteq \bigcup \GG_C$
Let $x \in A \cap B$.
Then by definition of intersection:
- $v \in A$ and $x \in B$
Hence by definition of union:
- $\exists D \in \GG_A: x \in D$
Analogically:
- $\exists E \in \GG_B: x \in E$
By definition of subset $D, E \in \BB$ and by definition of intersection $x \in D \cap E$.
Then by $(\text B 1)$:
- $\exists U \in \BB: x \in U \subseteq D \cap E$
By Set is Subset of Union/Set of Sets:
- $D \subseteq A$ and $E \subseteq B$
Then by Set Intersection Preserves Subsets:
- $D \cap E \subseteq A \cap B$
Hence by Subset Relation is Transitive:
- $U \subseteq A \cap B$
Then by definition of $\GG_C$:
- $U \in \GG_C$
Thus by definition of union:
- $x \in \bigcup \GG_C$
This ends the proof of inclusion.
Then by definition of set equality:
- $A \cap B = \bigcup \GG_C$
By definition of subset:
- $\GG_C \subseteq \BB$
Thus by definition of $\tau$:
- $A \cap B \in \tau$
$\Box$
Open Set Axiom $\paren {\text O 3 }$: Underlying Set is Element of Topology
By $(\text B 2)$ and definition of union:
- $\bigcup \BB = X$
Because $\BB \subseteq \BB$ by definition of $\tau$:
- $S \in \tau$
It remains to prove that $\BB$ is a basis of $T$.
Let $U$ be an open set of $S$.
Let $x$ be a point of $S$ such that $x \in U$
By definition of $\tau$ there exists $\GG \subseteq \BB$ such that:
- $U = \bigcup \GG$
By definition of union:
- $\exists A \in \GG: x \in A$
By definition of subset: $A \in \BB$
Thus by Set is Subset of Union:
- $x \in A \subseteq U$
$\Box$
All the open set axioms are fulfilled, and the result follows by definition of basis.
$\blacksquare$
Sources
- Mizar article TOPGEN_3:2