Theorem Topology.IsInducing.completelyNormalSpace

Modification history

2026-06-04 20:02
Mathlib/Topology/Separation/Regular.lean
chore(Topology): generalize `Topology.IsEmbedding.perfectlyNormalSpace` (#39576) …
Added Topology.IsInducing.completelyNormalSpaceView on Github →