Commit 2020-09-14 23:27 3d73bd86

feat(topology/algebra/ordered): monotone continuous function is homeomorphism, relative version (#4043) A function f : α → β restricts to a homeomorphism (Ioo a b) → β, if it (1) is order-preserving within the interval; (2) is continuous_on the interval; (3) tends to positive infinity at the right endpoint; and (4) tends to negative infinity at the left endpoint. The orders α, β are required to be conditionally complete, and the order on α must also be dense.