normed type neighborhood lemmas

[amolinamounier]

Motivation for this change

Split from #2023. Depends on #2024 and #2027.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md
• Merge Utility lemmas in filter.v #2024
• Merge New topology lemmas #2027

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

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

[affeldt-aist]

(not yet reviewed but rebased)

[affeldt-aist]

The statement of near_shiftE and nbhsDl are the same but on different structures that maybe ought to share an interface. This is an observation that has already been done for other lemmas, so maybe this is time to reconsider the hierarchy of mathematical structures to factorize code.

See
https://github.com/math-comp/analysis/blob/master/theories/normedtype_theory/tvs.v#L122-L128

[affeldt-aist]

The duplication of code is calling for a more in-depth review (which might end up in adding structures) so we postpone to the next release (fyi: @mkerjean )

[affeldt-aist]

Just a thought:
We long had PseudoMetricNormedZmod defined with a numDomainType parameter.
Recently, we have added PseudoMetricNormedZmod0 and made PseudoMetricNormedZmod derive from Metric.
In fact, as a consequence, many lemmas can be changed from PseudoMetricNormedZmod down to PseudoMetricNormedZmod0 without impacting the code.
Which makes me wonder whether we shouldn't make PseudoMetricNormedZmod have a numFieldType as a parameter instead of sticking to numDomainType: this actually comes in the way when trying to refactor the code as hinted at in this conversation.

[mkerjean]

I'm happy to do a review but I'm lacking a bit of context. Why are these lemmas duplicated ? What's the goal of this PR ?