ThmDex – An index of mathematical definitions, results, and conjectures.
Set of symbols
Alphabet
Deduction system
Theory
Zermelo-Fraenkel set theory
Set
Subset
Power set
Hyperpower set sequence
Hyperpower set
Hypersubset
Subset algebra
Definition D86
Topology
Formulation 0
Let $X$ be a D11: Set such that
(i) $\mathcal{P}(X)$ is the D80: Power set of $X$
A D11: Set $\mathcal{T} \subseteq \mathcal{P}(X)$ is a topology on $X$ if and only if
(1) \begin{equation} \emptyset, X \in \mathcal{T} \end{equation}
(2) \begin{equation} \forall \, \mathcal{S} \subseteq \mathcal{T} : \cup \mathcal{S} \in \mathcal{T} \end{equation}
(3) \begin{equation} \forall \, N \in 1, 2, 3, \ldots : \forall \, E_1, \dots, E_N \in \mathcal{T} : \bigcap_{n = 1}^N E_n \in \mathcal{T} \end{equation}
Formulation 1
Let $X$ be a D11: Set such that
(i) $\mathcal{P}(X)$ is the D80: Power set of $X$
A D11: Set $\mathcal{T} \subseteq \mathcal{P}(X)$ is a topology on $X$ if and only if
(1) \begin{equation} \emptyset, X \in \mathcal{T} \end{equation}
(2) \begin{equation} \forall \, \mathcal{S} \subseteq \mathcal{T} : \bigcup_{S \in \mathcal{S}} S \in \mathcal{T} \end{equation}
(3) \begin{equation} \forall \, N \in 1, 2, 3, \ldots : \forall \, E_1, \dots, E_N \in \mathcal{T} : \bigcap_{n = 1}^N E_n \in \mathcal{T} \end{equation}
Children
D1163: Bottom topology
D154: Pushforward topology
D2197: Set of topologies
D3591: Subtopology