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