Commit 2026-06-04 20:02 96c19134

View on Github →

chore(Topology): generalize Topology.IsEmbedding.perfectlyNormalSpace (#39576) Generalize theorem Topology.IsEmbedding.perfectlyNormalSpace to inducing maps. Generalize some other theorem along the way. Rename isGδ_induced to IsGδ.preimage, to match IsOpen.preimage and IsClosed.preimage.

Estimated changes

Modified Mathlib/Topology/Baire/LocallyCompactRegular.lean

added theorem IsGδ.baireSpace_of_t2Space_locallyCompactSpace

deleted theorem IsGδ.of_t2Space_locallyCompactSpace

Modified Mathlib/Topology/GDelta/Basic.lean

added theorem IsGδ.preimage

deleted theorem isGδ_induced

Modified Mathlib/Topology/Separation/GDelta.lean

added theorem Topology.IsEmbedding.t6Space

added theorem Topology.IsInducing.perfectlyNormalSpace

Modified Mathlib/Topology/Separation/PerfectlyNormal.lean

deleted theorem Topology.IsEmbedding.perfectlyNormalSpace

Modified Mathlib/Topology/Separation/Regular.lean

deleted theorem Topology.IsEmbedding.completelyNormalSpace

added theorem Topology.IsInducing.completelyNormalSpace