feat(topology/compact_open): convergence in the compact-open topology…

… can be checked on compact sets (#9240)

src/topology/compact_open.lean

@@ -101,10 +101,33 @@ continuous_iff_continuous_at.mpr $ assume ⟨f, x⟩ n hn,
   have (f, x) ∈ w, from ⟨image_subset_iff.mpr sv, xu⟩,
   mem_nhds_iff.mpr ⟨w, by assumption, by assumption, by assumption⟩
 
+lemma continuous_ev₁ [locally_compact_space α] (a : α) : continuous (λ f : C(α, β), f a) :=
+continuous_ev.comp (continuous_id.prod_mk continuous_const)
+
+instance [t2_space β] [locally_compact_space α] : t2_space C(α, β) :=
+⟨ begin
+    intros f₁ f₂ h,
+    obtain ⟨p, hp⟩ := not_forall.mp (mt continuous_map.ext h),
+    exact separated_by_continuous (continuous_ev₁ p) hp,
+  end ⟩
+
 end ev
 
 section Inf_induced
 
+lemma compact_open_le_induced (s : set α) :
+  (continuous_map.compact_open : topological_space C(α, β))
+  ≤ topological_space.induced (continuous_map.restrict s) continuous_map.compact_open :=
+begin
+  simp only [induced_generate_from_eq, continuous_map.compact_open],
+  apply generate_from_mono,
+  rintros b ⟨a, ⟨c, hc, u, hu, rfl⟩, rfl⟩,
+  refine ⟨coe '' c, hc.image continuous_subtype_coe, u, hu, _⟩,
+  ext f,
+  simp only [compact_open.gen, mem_set_of_eq, mem_preimage, continuous_map.coe_restrict],
+  rw image_comp f (coe : s → α),
+end
+
 /-- The compact-open topology on `C(α, β)` is equal to the infimum of the compact-open topologies
 on `C(s, β)` for `s` a compact subset of `α`.  The key point of the proof is that the union of the
 compact subsets of `α` is equal to the union of compact subsets of the compact subsets of `α`. -/
@@ -113,35 +136,74 @@ lemma compact_open_eq_Inf_induced :
   = ⨅ (s : set α) (hs : is_compact s),
     topological_space.induced (continuous_map.restrict s) continuous_map.compact_open :=
 begin
+  refine le_antisymm _ _,
+  { refine le_binfi _,
+    exact λ s hs, compact_open_le_induced s },
   simp only [← generate_from_Union, induced_generate_from_eq, continuous_map.compact_open],
-  congr' 1,
-  ext m,
+  apply generate_from_mono,
+  rintros _ ⟨s, hs, u, hu, rfl⟩,
   rw mem_bUnion_iff',
-  split,
-  { rintros ⟨s, hs, u, hu, rfl⟩,
-    refine ⟨s, hs, compact_open.gen univ u, _⟩,
-    refine ⟨⟨univ, is_compact_iff_is_compact_univ.mp hs, u, hu, rfl⟩, _⟩,
-    ext f,
-    simp only [compact_open.gen, mem_set_of_eq, mem_preimage, continuous_map.coe_restrict],
-    rw image_comp f (coe : s → α),
-    simp },
-  { rintros ⟨s, hs, sb, ⟨s', hs', u, hu, rfl⟩, rfl⟩,
-    refine ⟨coe '' s', hs'.image continuous_subtype_coe, u, hu, _⟩,
-    ext f,
-    simp only [compact_open.gen, coe_restrict, mem_set_of_eq, preimage_set_of_eq,
-      image_subset_iff],
-    rw preimage_comp },
+  refine ⟨s, hs, _, ⟨univ, is_compact_iff_is_compact_univ.mp hs, u, hu, rfl⟩, _⟩,
+  ext f,
+  simp only [compact_open.gen, mem_set_of_eq, mem_preimage, continuous_map.coe_restrict],
+  rw image_comp f (coe : s → α),
+  simp
 end
 
+/-- For any subset `s` of `α`, the restriction of continuous functions to `s` is continuous as a
+function from `C(α, β)` to `C(s, β)` with their respective compact-open topologies. -/
+lemma continuous_restrict (s : set α) : continuous (λ F : C(α, β), F.restrict s) :=
+by { rw continuous_iff_le_induced, exact compact_open_le_induced s }
+
 lemma nhds_compact_open_eq_Inf_nhds_induced (f : C(α, β)) :
   𝓝 f = ⨅ s (hs : is_compact s), (𝓝 (f.restrict s)).comap (continuous_map.restrict s) :=
 by { rw [compact_open_eq_Inf_induced], simp [nhds_infi, nhds_induced] }
 
+lemma tendsto_compact_open_restrict {ι : Type*} {l : filter ι} {F : ι → C(α, β)} {f : C(α, β)}
+  (hFf : filter.tendsto F l (𝓝 f)) (s : set α) :
+  filter.tendsto (λ i, (F i).restrict s) l (𝓝 (f.restrict s)) :=
+(continuous_restrict s).continuous_at.tendsto.comp hFf
+
 lemma tendsto_compact_open_iff_forall {ι : Type*} {l : filter ι} (F : ι → C(α, β)) (f : C(α, β)) :
-  filter.tendsto F l (nhds f)
+  filter.tendsto F l (𝓝 f)
   ↔ ∀ s (hs : is_compact s), filter.tendsto (λ i, (F i).restrict s) l (𝓝 (f.restrict s)) :=
 by { rw [compact_open_eq_Inf_induced], simp [nhds_infi, nhds_induced, filter.tendsto_comap_iff] }
 
+/-- A family `F` of functions in `C(α, β)` converges in the compact-open topology, if and only if
+it converges in the compact-open topology on each compact subset of `α`. -/
+lemma exists_tendsto_compact_open_iff_forall [locally_compact_space α] [t2_space α] [t2_space β]
+  {ι : Type*} {l : filter ι} [filter.ne_bot l] (F : ι → C(α, β)) :
+  (∃ f, filter.tendsto F l (𝓝 f))
+  ↔ ∀ (s : set α) (hs : is_compact s), ∃ f, filter.tendsto (λ i, (F i).restrict s) l (𝓝 f) :=
+begin
+  split,
+  { rintros ⟨f, hf⟩ s hs,
+    exact ⟨f.restrict s, tendsto_compact_open_restrict hf s⟩ },
+  { intros h,
+    choose f hf using h,
+    -- By uniqueness of limits in a `t2_space`, since `λ i, F i x` tends to both `f s₁ hs₁ x` and
+    -- `f s₂ hs₂ x`, we have `f s₁ hs₁ x = f s₂ hs₂ x`
+    have h : ∀ s₁ (hs₁ : is_compact s₁) s₂ (hs₂ : is_compact s₂) (x : α) (hxs₁ : x ∈ s₁)
+      (hxs₂ : x ∈ s₂), f s₁ hs₁ ⟨x, hxs₁⟩ = f s₂ hs₂ ⟨x, hxs₂⟩,
+    { rintros s₁ hs₁ s₂ hs₂ x hxs₁ hxs₂,
+      haveI := is_compact_iff_compact_space.mp hs₁,
+      haveI := is_compact_iff_compact_space.mp hs₂,
+      have h₁ := (continuous_ev₁ (⟨x, hxs₁⟩ : s₁)).continuous_at.tendsto.comp (hf s₁ hs₁),
+      have h₂ := (continuous_ev₁ (⟨x, hxs₂⟩ : s₂)).continuous_at.tendsto.comp (hf s₂ hs₂),
+      exact tendsto_nhds_unique h₁ h₂ },
+    -- So glue the `f s hs` together and prove that this glued function `f₀` is a limit on each
+    -- compact set `s`
+    have hs : ∀ x : α, ∃ s (hs : is_compact s), s ∈ 𝓝 x,
+    { intros x,
+      obtain ⟨s, hs, hs'⟩ := exists_compact_mem_nhds x,
+      exact ⟨s, hs, hs'⟩ },
+    refine ⟨lift_cover' _ _ h hs, _⟩,
+    rw tendsto_compact_open_iff_forall,
+    intros s hs,
+    rw lift_cover_restrict',
+    exact hf s hs }
+end
+
 end Inf_induced
 
 section coev