Existence and Uniqueness of Generated Topology
 | This page has been identified as a candidate for refactoring of basic complexity. In particular: Separate pages for proofs, as they are linked to individually Until this has been finished, please leave {{Refactor}} in the code.
New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Refactor}} from the code. |
Theorem
Let $X$ be a set.
Let $\SS \subseteq \powerset X$ be a subset of the power set of $X$.
Then there exists a unique topology $\map \tau \SS$ on $X$ such that:
- $(1): \quad \SS \subseteq \map \tau \SS$.
- $(2): \quad$ For any topology $\TT$ on $X$, the implication $\SS \subseteq \TT \implies \map \tau \SS \subseteq \TT$ holds.
Proof
Existence
Define:
- $\mathbb E = \leftset {\TT \subseteq \powerset X: \SS \subseteq \TT}$ and $\TT$ is a topology on $\rightset X$
Since $\powerset X$ is a topology on $X$, it follows that $\mathbb E$ is non-empty.
Hence, we can define:
- $\ds \map \tau \SS = \bigcap \mathbb E$
It follows that $\map \tau \SS$ is a topology on $X$.
By Intersection is Largest Subset: General Result, it follows that $\SS \subseteq \map \tau \SS$.
By Intersection is Subset: General Result, it follows that if $\SS \subseteq \TT$ and $\TT$ is a topology on $X$, then $\map \tau \SS \subseteq \TT$.
$\Box$
Uniqueness
Suppose that $\TT_1$ and $\TT_2$ are both topologies on $X$ satisfying conditions $(1)$ and $(2)$.
By condition $(1)$, we have $\SS \subseteq \TT_2$; hence, we can apply condition $(2)$ to conclude that:
- $\TT_1 \subseteq \TT_2$
Similarly:
- $\TT_2 \subseteq \TT_1$
By definition of set equality:
- $\TT_1 = \TT_2$
$\blacksquare$