Commit 2023-10-10 21:36 69c11afc

feat: nowhere dense and meagre sets (#7180) 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.