mathlib

d9a7d05d - chore(topology/algebra/ordered): add `order_iso.to_homeomorph` (#5111)

chore(topology/algebra/ordered): add `order_iso.to_homeomorph` (#5111) * Replace `homeomorph_of_strict_mono_surjective` with `order_iso.to_homeomorph` and `order_iso.continuous`. * Drop `continuous_at_of_strict_mono_surjective` in favor of `order_iso.to_homeomorph`. * Use notation for `nhds_within` here and there.