Theorem IsGδ.of_t2Space_locallyCompactSpace

Modification history

2026-06-04 20:02

Mathlib/Topology/Baire/LocallyCompactRegular.lean

chore(Topology): generalize `Topology.IsEmbedding.perfectlyNormalSpace` (#39576) …

Deleted IsGδ.of_t2Space_locallyCompactSpace View on Github →

2026-01-07 10:31

Mathlib/Topology/Baire/LocallyCompactRegular.lean

feat: a dense Gdelta subset of a Baire space is Baire. (#32674) …

Added IsGδ.of_t2Space_locallyCompactSpace View on Github →