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]

Definitions need to be documented, but I guess you were planning to do it later.

[affeldt-aist]

Did you consider using an HB.mixin for this property? Since, for example, numDomainType is an instance, that might simplify the presentation of later lemmas.

[t6s]

Turning this part into a structure using HB is actually good.
I somehow thought that would not work, but let us see by trying it. I will update the code in that way.

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

I guess this lemma will have the same usability problem as setUitv1 and setU1itv (see issue #1914 ) and that specialization with easy-to-understand names will be called for. On the other hand, it is not used in this PR, so it could be separated in a different PR to simplify the review of this PR (#1848).

[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?