feat(topology/compact_open): the family of constant maps collectively form a continuous map (#8721)
feat(topology/compact_open): the family of constant maps collectively form a continuous map (#8721)






leanprover-community/mathlib,leanprover-community/mathlib