← All papers
On the Number of Distinct Topological Bases of a Finite Set of Size $N$
math.CO
Sep 12, 2026 · v1
cs.LO math.GN
TL;DR
Formalizes in Lean 4 / Mathlib the count of topological bases on a finite set via minimal open neighborhoods.
Abstract
For a finite set $S$ with $\lvert S\rvert = N$, the number of families $\mathcal{B} \subseteq \mathcal{P}(S)$ that are topological bases is $\#(N) = \sum_{\mathcal{T} \in \operatorname{Top}(S)} 2^{\lvert\mathcal{T}\rvert - \lvert\mathcal{M}_{\mathcal{T}}\rvert}$, 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`.
Problem
Counting the number of families B ⊆ P(S) that form a topological basis on a finite set S of size N.
Approach
The count is expressed as a sum over topologies T on S of 2^(|T| - |M_T|), where M_T is the canonical minimal basis of minimal open neighborhoods. The key characterization is that bases generating T are exactly the sets B with M_T ⊆ B ⊆ T. The identity is proved formally in Lean 4 / Mathlib in CARDB.lean, with small-N tables and asymptotic bounds in separate files.
Results
The counting identity is established, small-N values are verified, and a discrete-dominance sandwich giving asymptotic bounds is proved.