Commit 2020-12-03 01:03 d9a7d05d
View on Github →chore(topology/algebra/ordered): add order_iso.to_homeomorph
(#5111)
- Replace
homeomorph_of_strict_mono_surjective
withorder_iso.to_homeomorph
andorder_iso.continuous
. - Drop
continuous_at_of_strict_mono_surjective
in favor oforder_iso.to_homeomorph
. - Use notation for
nhds_within
here and there.