mathlib3

9b333b26 - feat(topology/algebra/continuous_monoid_hom): `to_continuous_map` is a `closed_embedding` (#12217)

feat(topology/algebra/continuous_monoid_hom): `to_continuous_map` is a `closed_embedding` (#12217) This PR proves that `to_continuous_map : continuous_monoid_hom A B → C(A, B)` is a `closed_embedding`. This will be useful for showing that the Pontryagin dual is locally compact.