On the Number of Distinct Topological Bases of a Finite Set of Size $N$

Abstract

For a finite set $S$ with $|S|=N$, the number of families $\mathcal{B}\subseteq \mathcal{P}(S)$ that are topological bases is $\#(N)={\sum }_{\mathcal{T}\in \mathrm{Top}(S)}{2}^{|\mathcal{T}|-|{\mathcal{M}}_{\mathcal{T}}|}$, where ${\mathcal{M}}_{\mathcal{T}}$ is the canonical minimal basis of minimal open neighborhoods. The identity is proved in Lean 4 / Mathlib (`CARDB.lean`): bases generating $\mathcal{T}$ are exactly the sets with ${\mathcal{M}}_{\mathcal{T}}\subseteq \mathcal{B}\subseteq \mathcal{T}$. The small-$N$ table and the discrete-dominance sandwich are proved in `CARDB/SmallN.lean` and `CARDB/Asymptotics.lean`.

arXiv comment29 pages