mathlib3

3339976e - refactor(topology/constructions): rename `continuous_subtype_mk` (#16223)

refactor(topology/constructions): rename `continuous_subtype_mk` (#16223) * rename `continuous_subtype_mk` to `continuous.subtype_mk` to allow dot notation; * add `continuous.subtype_map`.