Theorem not_isMeagre_of_mem_residual

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) …
Added not_isMeagre_of_mem_residualView on Github →