Theorem Topology.IsEmbedding.perfectlyNormalSpace

Modification history

2026-06-04 20:02
Mathlib/Topology/Separation/PerfectlyNormal.lean
chore(Topology): generalize `Topology.IsEmbedding.perfectlyNormalSpace` (#39576) …
Deleted Topology.IsEmbedding.perfectlyNormalSpaceView on Github →
2026-05-17 12:59
Mathlib/Topology/Separation/PerfectlyNormal.lean
feat(Topology): subspace of a perfectly normal space is perfectly normal (#38533) …
Added Topology.IsEmbedding.perfectlyNormalSpaceView on Github →