mathlib3

fe00980a - feat(topology/compact_open): β ≃ₜ C(α, β) if α has a single element (#6946)