separating filters

[zstone1]

Continuing with #1167, this puts all the stuff about filters into a separate file in classical. It ends up being around 1500, which is a very comfortable file size compared to the 7000+ from topology.v. I moved the docs around, hopefully I didn't miss anything.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

Maybe for the chaneglog the following is enough (I didn't commit because it calls for a rebase):

# Changed:

- `theories/topology.v` split into `classical/filter.v` and `theories/topology.v`

- moved from `topology.v` to `mathcomp_extra.v`:
  + lemma `and_prop_in`

- moved from `topology.v` to `set_interval.v`:
  + lemmas `bigmax_geP`, `bigmax_gtP`, `bigmin_leP`, `bigmin_ltP`
  + lemmas `mem_inc_segment`, `mem_inc_segment`

[zstone1]

rebased and changelog updated

[affeldt-aist]

Start looking good to me: splitting also contributed to make the doc shorter and more readable (no need for toc anymore), we spotted deadcode and potentially improved the naming of a few identifiers (granted these are micro improvements---you may want to double-check them though).

[affeldt-aist]

For me, it is ok. I made a last commit moving a few lemmas further down the hierarchy of files (in particular, bigmin/max lemmas looked a bit out of place in set_interval.v). However, I see that the PR has been marked as "bug" and @proux01 tagged. Is it because of the failing CI? (It has been red for some time but apparently because of third-party packages.)

[zstone1]

Yeah, I guess I wanted to be sure that I hadn't broken anything by moving stuff across packages. But you're right the build failures are the expected ones. Thanks for picking through this. It's a bit grueling, but you definitely improved things.