Theorem IsGδ.baireSpace_of_dense

Modification history

2026-01-07 10:31
Mathlib/Topology/Baire/Lemmas.lean
feat: a dense Gdelta subset of a Baire space is Baire. (#32674) …
Added IsGδ.baireSpace_of_denseView on Github →