mathlib

26d0a538 - fix(topology/continuous_function/basic): use `old_structure_cmd` to define `continuous_map_class` (#16164)

fix(topology/continuous_function/basic): use `old_structure_cmd` to define `continuous_map_class` (#16164) We fix `continuous_map_class` to use `old_structure_cmd`, and also fix the documentation of `fun_like` and `equiv_like` to specify that this should be done systematically for new morphism type classes. Without this, we get a `to_fun_like` field in the newly created class which then creates diamonds. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>