Commit 2024-09-19 08:44 74fc63fa

View on Github →

feat(LocallyCompact): generalize *Embedding.locallyCompactSpace (#16291) to Inducing maps

Estimated changes

Modified Mathlib/Topology/Compactness/LocallyCompact.lean

added theorem Inducing.locallyCompactSpace