mathlib3

3d73bd86 - feat(topology/algebra/ordered): monotone continuous function is homeomorphism, relative version (#4043)

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.