错行

#拓扑

关于滤子：极限及“最终”模态词诱导

起因是听说 Lean 现在的 mathlib 中实数是依靠滤子定义的（虽然实际搜索了一下发现当前版本还是改为用 Cauchy 序列定义）。…
关于滤子：极限及“最终”模态词诱导

#点集拓扑

点集拓扑以开集为基本工具，研究空间的连续性与整体形状，刻画连通性、紧性与分离性等基本拓扑性质。

#点集拓扑