[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] \section{Topological spaces} We define topological spaces using neighbourhood filters. A topological space is a set $X$ with a function $\mathcal{F}:X \to \mathcal{P}(\mathcal{P}(X))$ from $X$ to the double power set of $X$ such that * $\mathcal{F}(x)$ is a filter for all $x:X$ * For all $x:X$ and for all $N:\mathcal{P}(X)$, $N \in_{\mathcal{P}(X)} \mathcal{F}(x)$ implies that $x \in_X N$ * For all $x:X$ and for all $N:\mathcal{P}(X)$, $N \in_{\mathcal{P}(X)} \mathcal{F}(x)$ implies that $\left(\sum_{z:X} (z \in_X N) \times (N \in_{\mathcal{P}(X)} \mathcal{F}(z))\right)_\Omega \in_{\mathcal{P}(X)} \mathcal{F}(x)$ \section{References} * [https://math.stackexchange.com/questions/2769867/characterization-of-topology/2771383#2771383](https://math.stackexchange.com/questions/2769867/characterization-of-topology/2771383#2771383) * [https://math.stackexchange.com/questions/4077008/defining-a-topology-in-terms-of-filter-neighbourhoods](https://math.stackexchange.com/questions/4077008/defining-a-topology-in-terms-of-filter-neighbourhoods) category: redirected to nlab