feat(topology/compact_open): express the compact-open topology as an Inf of topologies

src/topology/compact_open.lean

@@ -46,7 +46,23 @@ variables [topological_space α] [topological_space β] [topological_space γ]
 
 def compact_open.gen (s : set α) (u : set β) : set C(α,β) := {f | f '' s ⊆ u}
 
--- The compact-open topology on the space of continuous maps α → β.
+variables (β)
+/-- For a fixed `s : set α`, the set of subsets of `C(α, β)` of the form `{f | f '' s ⊆ u}`, as `u`
+varies over the open subsets of `β`. -/
+def uniform_on.gen (s : set α) : set (set C(α, β)) :=
+{m | ∃ (u : set β) (hu : is_open u), m = compact_open.gen s u}
+
+/-- For a fixed `s : set α`, the topology on `C(α, β)` generated by `uniform_on.gen β s`; morally,
+the topology of "uniform convergence on `s`".  Not an instance because it varies with `s`. -/
+def uniform_on (s : set α) : topological_space C(α, β) :=
+topological_space.generate_from (uniform_on.gen β s)
+variables {β}
+
+private lemma is_open_uniform_on_gen (s : set α) {u : set β} (hu : is_open u) :
+  (uniform_on β s).is_open (compact_open.gen s u) :=
+topological_space.generate_open.basic _ (by dsimp [uniform_on.gen, mem_set_of_eq]; tauto)
+
+/-- The compact-open topology on the space of continuous maps `α → β`. -/
 instance compact_open : topological_space C(α, β) :=
 topological_space.generate_from
   {m | ∃ (s : set α) (hs : is_compact s) (u : set β) (hu : is_open u), m = compact_open.gen s u}
@@ -55,6 +71,20 @@ private lemma is_open_gen {s : set α} (hs : is_compact s) {u : set β} (hu : is
   is_open (compact_open.gen s u) :=
 topological_space.generate_open.basic _ (by dsimp [mem_set_of_eq]; tauto)
 
+/-- The compact-open topology is equal to the infimum, as `s` varies over the compact subsets of
+`α`, of the topologies of uniform convergence on `s`. -/
+lemma compact_open_eq_Inf_uniform_on :
+  continuous_map.compact_open = ⨅ (s : set α) (hs : is_compact s), uniform_on β s :=
+begin
+  transitivity
+    topological_space.generate_from (⋃ (s : set α) (hs : is_compact s), uniform_on.gen β s),
+  { rw continuous_map.compact_open,
+    congr' 1,
+    ext s,
+    simp [uniform_on.gen] },
+  simp [generate_from_Union, uniform_on]
+end
+
 section functorial
 
 variables {g : β → γ} (hg : continuous g)