Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-22 10:50 68efb10c

View on Github →

refactor(topology/*): Hom classes for continuous maps/homs (#11909) Add

  • continuous_map_class
  • bounded_continuous_map_class
  • continuous_monoid_hom_class
  • continuous_add_monoid_hom_class
  • continuous_map.homotopy_class to follow the fun_like design. Deprecate lemmas accordingly. Also rename a few fields to match the convention in the rest of the library.

Estimated changes