Mathlib v3 is deprecated. Go to Mathlib v4

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 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.

Estimated changes