关于大小为 $N$ 的有限集的不同拓扑基的数量
On the Number of Distinct Topological Bases of a Finite Set of Size $N$
浏览论文内容
中文总结 AI 辅助
本文用 Lean 4 形式化证明了有限集拓扑基计数恒等式，并给出小 N 表格与渐近夹逼结果。
中文摘要 AI 辅助
对于满足 $\lvert S\rvert = N$ 的有限集 $S$，作为拓扑基的族 $\mathcal{B} \subseteq \mathcal{P}(S)$ 的数量为 $\\#(N) = \sum_{\mathcal{T} \in \operatorname{Top}(S)} 2^{\lvert\mathcal{T}\rvert - \lvert\mathcal{M}_{\mathcal{T}}\rvert}$，其中 $\mathcal{M}_{\mathcal{T}}$ 是最小开邻域的规范最小基。该恒等式在 Lean 4 / Mathlib 中证明（见 `this http URL`）：生成 $\mathcal{T}$ 的基恰好是满足 $\mathcal{M}_{\mathcal{T}} \subseteq \mathcal{B} \subseteq \mathcal{T}$ 的集合。小 $N$ 的表格和离散支配夹逼在 `CARDB/SmallN.lean` 和 `CARDB/Asymptotics.lean` 中证明。
英文摘要
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`.
发表机构
- Catskills Research Company（卡茨基尔研究公司）
机构由 AI 辅助整理，请以论文原文为准。
