mathlib3

2b6924d5 - feat(topology/algebra/ordered): conditions for a strictly monotone function to be a homeomorphism (#3843)

feat(topology/algebra/ordered): conditions for a strictly monotone function to be a homeomorphism (#3843) If a strictly monotone function between linear orders is surjective, it is a homeomorphism. If a strictly monotone function between conditionally complete linear orders is continuous, and tends to `+∞` at `+∞` and to `-∞` at `-∞`, then it is a homeomorphism. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Order.20topology) Co-authored by: Yury Kudryashov <urkud@ya.ru> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>