[Merged by Bors] - feat: nowhere dense and meagre sets

[grunweg]

Define nowhere dense and meagre sets and show their basic properties.
Meagre sets are defined as the complement of comeagre(=residual) sets
(and shown to be equivalent to the standard definition); we deduce their API from the API for comeagre sets.

---

I'm still pretty new to Lean, hence am open to learning further ways to golf this! :-)
If mathlib prefers American English, I can adjust 😂

[grunweg]

One sorry remaining, which should be a simple lemma. (Help welcome in filling this; otherwise I'll do it on Monday or so.)
Otherwise ready for review.

[grunweg]

Thanks for the fast review.

I've addressed all comments. I've also filled in the last sorry and added the missing import.

[Felix-Weilacher]

A few comments

• I think starting a new file for Baire category stuff makes sense, but Topology.Meagre is not a good name. Meagreness itself is not distinct enough from residual to have its own file, I think. Maybe Topology.Baire? It might also be correct to put this stuff in Topology.Gdelta. I'm not sure.
• Because of how central filters are in mathlib, I think it makes more sense to define meagre as "my complement is residual", and then prove that this is equivalent to being contained in a countable union of nowhere dense sets.

[grunweg]

Sure, I can change both. I'll make these changes once a full review has been performed.

[grunweg]

@Felix-Weilacher I have addressed your comments, and also significantly golfed the proofs.

I'm not sure if GDelta.lean is the best file/that file should be renamed now, but it's certainly a decent place.

[grunweg]

Friendly 15-day review ping - just in case this slipped under the radar.

I have rebased on latest master and golfed the proof another time; I don't see much leeway of squeezing them further. Suggestions welcome.

[alreadydone]

LGTM except for some docstrings / declaration names / golfs

[grunweg]

Thank you for the fast review. I've addressed all comments.

[grunweg]

Thank you again. I have update the code.

[alreadydone]

Thanks!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by alreadydone.

[github-actions]

🚀 Pull request has been placed on the maintainer queue by alreadydone.

[ocfnash]

Thanks!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style