Finite Weight Space has Basis equal to Image of Mapping of Intersections
Theorem
Let $T = \left({X, \tau}\right)$ be a topological space with finite weight.
Then there exist a basis $\mathcal B$ of $T$ and a mapping $f:X \to \tau$ such that
- $\mathcal B = \operatorname{Im} \left({f}\right)$ and
- $\forall x \in X: \left({x \in f \left({x}\right) \land \forall U \in \tau: x \in U \implies f \left({x}\right) \subseteq U}\right)$.
where $\operatorname{Im} \left({f}\right)$ denotes the image of $f$.
Proof
By definition of weight there exists a basis $\mathcal B$ such that
- $\left\vert {\mathcal B} \right\vert = w \left({T}\right)$
where
- $w \left({T}\right)$ denotes the weight of $T$,
- $\left\vert {\mathcal B} \right\vert$ denotes the cardinality of $\mathcal B$.
By assumption that weight is finite:
- $\left\vert {\mathcal B} \right\vert$ is finite.
Then by Cardinality of Set is Finite iff Set is Finite:
- $\mathcal B$ is finite.
Define a mapping $f: X \to \mathcal P \left({X}\right)$
- $(1): \quad \forall x \in X: f \left({x}\right) = \bigcap \left\{{U \in \mathcal B: x \in U}\right\}$.
By definition of subset:
- $\forall x \in X: \left\{{U \in \mathcal B: x \in U}\right\} \subseteq \mathcal B$.
By Subset of Finite Set is Finite
- $\forall x \in X: \left\{{U \in \mathcal B: x \in U}\right\}$ is finite.
Then by General Intersection Property of Topological Space
- $\forall x \in X: \bigcap \left\{{U \in \mathcal B: x \in U}\right\} \in \tau$.
So:
- $f: X \to \tau$.
We will prove that
- $(2): \quad \forall x \in X: \left({x \in f \left({x}\right) \land \forall U \in \tau: x \in U \implies f \left({x}\right) \subseteq U}\right)$.
Let $x \in X$.
By $(1)$:
- $f \left({x}\right) = \bigcap \left\{{U \in \mathcal B: x \in U}\right\}$.
Thus by definition of intersection:
- $x \in f \left({x}\right)$.
Let $U$ be an open set of $T$.
Let $x \in U$.
By definition of basis
- $\exists V \in \mathcal B: x \in V \subseteq U$.
Then
- $V \in \left\{{U \in \mathcal B: x \in U}\right\}$.
Hence by Intersection is Subset:
- $f \left({x}\right) \subseteq V$.
Thus by Subset Relation is Transitive
- $f \left({x}\right) \subseteq U$.
This ends the proof of $(2)$.
We will prove that $\operatorname{Im} \left({f}\right)$ is a basis of $T$.
By $f: X \to \tau$ and definition of image
- $\operatorname{Im} \left({f}\right) \subseteq \tau$.
Let $U$ be an open set of $T$.
Let $x$ be a point $x \in X$ such that
- $x \in U$.
By $(2)$:
- $f \left({x}\right) \in \operatorname{Im} \left({f}\right) \land x \in f \left({x}\right) \subseteq U$.
By definition of basis this ends the proof of basis.
Thus the result.
$\blacksquare$
Sources
- Mizar article TOPGEN_2:15