Normal Spaces via Urysohn's Lemma as a Lifting Property
General Topology
2026-02-13 v1
Abstract
We present a translation of Urysohn's description of normal spaces (as those where disjoint closed subsets are separated by a continuous function) into the language of lifting properties in , correcting a frequently-cited previous erroneous translation. We also present a translation of the definition of hereditarily normal spaces as those in which every open subspace is normal, by directly 'mapping' the translation of the usual description of normal spaces.
Cite
@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}
}
Comments
3 pages, 6 figures, formalization in Lean in terms of existing definitions in Mathlib at https://github.com/robertmaxton42/mathlib4/tree/separation