feat: port Topology.CompactOpen (#2123)

Co-authored-by: Arien Malec <arien.malec@gmail.com>
Co-authored-by: adamtopaz <github@adamtopaz.com>

Author: 3 people

Mathlib.lean

@@ -1038,6 +1038,7 @@ import Mathlib.Topology.Basic
 import Mathlib.Topology.Bornology.Basic
 import Mathlib.Topology.Bornology.Constructions
 import Mathlib.Topology.Bornology.Hom
+import Mathlib.Topology.CompactOpen
 import Mathlib.Topology.Connected
 import Mathlib.Topology.Constructions
 import Mathlib.Topology.ContinuousFunction.Basic