# 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 individuallyUntil this has been finished, please leave
`{{Refactor}}` in the code.
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$