add itv_closureE, itv_interiorE, and helper lemmas

[t6s]

Motivation for this change

Reviewing PR #1674 , it was noticed that there is not much theory
connecting closure/interior operators and set-intervals.
This PR adds lemmas to amend that, especially itv_interiorE and itv_closureE
stating that the interior/closure of an interval is an open/closed interval respectively,
for intervals in realFieldType.

This should resolve the following comment:
https://github.com/math-comp/analysis/pull/1674/changes/BASE..34697b2642259157cd3678e64092864dcd0ca4ef#r2685444293

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• 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]

For the sake of making progress with this PR, couldn't the part about classical_sets.v be a different PR? It looks pretty uncontroversial and could be merged quickly (this includes new lemmas and also the moving of the scope declarations for relations).

[affeldt-aist]

There a few lemmas in topology_structure.v (closureEbigcap_itvcy, interiorEbigcup_itvNyc, closureEbigcap_itvcc, interiorEbigcup_itvcc) that look like they could be PRed independently.
By the way, I was surprised to see that in these lemmas the variable A is used both as a set and
as an interval bound. Isn't that surprising and deserving a comment?

[affeldt-aist]

This PR is definitely useful (as exemplified by PR #1910 which is a special case as you rightfully observed, sorry about the duplicate, my bad).

I made a couple of requests to split out a few things that look like they could be PRed independently. The goal is twofold.

On the one hand, additions to classical_sets.v, topology_structure.v can be merged quickly; the addition of setUitv2 might have the same issue as we had with setUitv1/setU1itv which can be solved by a naming discussion that could take a bit more time so an individual PR would help.

On the other hand, the main addition about endlessness and order-density still needs to be experimented using HB.mixin's (as we already discussed). I am confident it will work out great but in any case this is a substantial addition to unstable.v that will need to be backported to MathComp at some point. I think that reducing this PR to endlessness and order-density will have the advantage of making it clearer when doing the HB.mixin experiment and the backport.

What do you think?

[t6s]

Thanks for suggestions.

I will separate some suggested parts into separate PRs.

setUitv1 and setU1itv are PRed as #1864.
There is an issue about an additional parameter, which will be discussed at #1914.

I will add a short comment at closureEbigcap_itvcy, etc. about their use of
intervals in powerset lattices.

Turning endless and dense orders into HB structures is a bigger change,
but necessary at some point in completing this PR.
I will PR it first to math-comp.

Additionally, I want to generalize statements about closures a bit to
handle also extended reals.

Because of the last two points, I turn this PR into a draft for now.

[affeldt-aist]

Is it ok for me to rebase this PR?

[affeldt-aist]

The lemmas provided by this PR are definitely useful.
I find the way the formalization is carried out clever.
There is the pending question of using HB for endlessness and density.
This is deferred to a MathComp PR under review
(math-comp/math-comp#1597, @CohenCyril).
The impact of potential changes is properly mitigated by the use of modules.
Provided the code is revised with MathComp PR 1597 is merge, it is ok
for me to merge this PR for the time being.

@holgerthies , @IshiguroYoshihiro : you might want to take a look

Thanks a lot @t6s !

[affeldt-aist]

I forgot to merge this one.
@t6s is it still ok with you? (I mean, despite the draft PR math-comp/math-comp#1597)

[t6s]

Looks okay. I am planning some additions, but they will be in another PR.