mathlib

68efb10c - refactor(topology/*): Hom classes for continuous maps/homs (#11909)

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.