Theorem perfectlyNormalSpace_iff_forall_isClosed_preimage_zero

Modification history

2026-05-17 12:59
Mathlib/Topology/Separation/PerfectlyNormal.lean
feat(Topology): subspace of a perfectly normal space is perfectly normal (#38533) …
Added perfectlyNormalSpace_iff_forall_isClosed_preimage_zeroView on Github →