Commit 2020-08-26 16:20 2b6924d5

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 Co-authored by: Yury Kudryashov urkud@ya.ru