Theorem not_isMeagre_of_isGδ_of_dense

Modification history

2025-08-14 11:59
Mathlib/Topology/Baire/Lemmas.lean
feat(Topology/Baire/Lemmas): residual sets in nonempty Baire spaces are not meagre (#28363) …
Modified not_isMeagre_of_isGδ_of_denseView on Github →
2025-08-07 17:04
Mathlib/Topology/Baire/Lemmas.lean
feat(Topology/Baire/Lemmas): In a nonempty Baire space, any dense GDelta set is not meagre (#27471) …
Added not_isMeagre_of_isGδ_of_denseView on Github →