Scifaro

中文

正规空间论述：以乌里森堡引理形式的提升性

一般拓扑 2026-02-13 v1

作者: Robert Maxton

在 arXiv 上查看 ↗ PDF ↗

摘要

本文将乌里森堡对正规空间的描述（即两两不相交的闭子集可被连续函数分离）翻译为 $\mathbf{Top}$ 中的提升性语言，纠正了常被引用的以往错误翻译。我们还将可分离正规空间的定义（即每个开子空间都是正规的）翻译为提升性语言，通过直接'映射'正规空间翻译的常规描述来实现。

关键词

正规空间乌里森堡引理提升性拓扑空间

引用

@article{arxiv.2602.11178,
  title  = {Normal Spaces via Urysohn's Lemma as a Lifting Property},
  author = {Robert Maxton},
  journal= {arXiv preprint arXiv:2602.11178},
  year   = {2026}
}

备注

3 pages, 6 figures, formalization in Lean in terms of existing definitions in Mathlib at https://github.com/robertmaxton42/mathlib4/tree/separation