Commit 2022-02-23 20:58 9b333b26
View on Github →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.