Theorem isGδ_induced

Modification history

2026-06-04 20:02
Mathlib/Topology/GDelta/Basic.lean
chore(Topology): generalize `Topology.IsEmbedding.perfectlyNormalSpace` (#39576) …
Deleted isGδ_inducedView on Github →
2026-01-07 10:31
Mathlib/Topology/GDelta/Basic.lean
feat: a dense Gdelta subset of a Baire space is Baire. (#32674) …
Added isGδ_inducedView on Github →