Commit 2026-05-17 12:59 bf8b279c

View on Github →

feat(Topology): subspace of a perfectly normal space is perfectly normal (#38533) The mains theorems proved in this PR are

A topological space is perfectly normal iff every closed set is the zero set of a continuous function taking values in the unit interval.
Every subspace of a perfectly normal space is perfectly normal.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Constructions.lean

added theorem IsClosed.image_val

added theorem IsOpen.image_val

Modified Mathlib/Topology/Maps/Basic.lean

added theorem Topology.IsInducing.image_eq_isClosed_inter_range

added theorem Topology.IsInducing.image_eq_isOpen_inter_range

Modified Mathlib/Topology/Separation/GDelta.lean

Modified Mathlib/Topology/Separation/Hausdorff.lean

added theorem SeparatedNhds.of_finite

Created Mathlib/Topology/Separation/PerfectlyNormal.lean

added theorem Topology.IsEmbedding.perfectlyNormalSpace

added theorem perfectlyNormalSpace_iff_forall_isClosed_preimage_zero