Order topology

[zstone1]

With pointed stuff out of the way, we can start really mixing types for great good! The adds

• Order topology! A mixin that states the order and nbhss are compatible
• Some basic lemmas about order topologies (the zero-dimensional stuff is just an annoying thing I need for building cantor-space isomorphisms that also preserve order structure).
• A side note: order topologies are, at the moment, hausdorff since orders are anti-symmetric. This isn't terrible, but most other lemmas will generalize nicely once https://github.com/math-comp/math-comp/pull/1169 lands, and intervals are generalized.
• A order_topology alias for attaching the "induced order topology" to an ordered set
• A bunch of lemmas about intervals and sets
• Order instances for bool, nat, and realFieldType

Checklist

• [x] added corresponding entries in CHANGELOG_UNRELEASED.md

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

Ah but maybe rray_open was right in the first place since MathComp conventions require this format mainSymbol_unaryPredicate for unary predicate, this is open_lt and the like that we have to rename

[zstone1]

Yes, that makes sense. We'll have a chance to clean up the names as this order stuff evolves. I've pushed with

1. Moving the stuff from lebesgue into set_interval
2. I added a lemma that shows the definitions are related (but not equal! the converse is false).
3. Keeping the lray_open style names

[affeldt-aist]

Line 4082 "From mathcomp Require Import set_interval." can probably be removed

[affeldt-aist]

Ah, I almost forgot, should we take care of the renaming of, e.g., https://github.com/math-comp/analysis/blob/ad764a4d62d84c5d406eb9197431945f76ef5655/theories/normedtype.v#L1192 along this PR? What would be a better name for it that looks like lray_open? rlray_open?

[zstone1]

I was planning on doing that in a follow up where we rename and generalize from R to any order topology.