feat(topology/uniform_space/uniform_convergence): add lemma `tendsto_…

…locally_uniformly_iff_forall_tendsto` (#13201)

src/data/set/basic.lean

@@ -180,6 +180,10 @@ theorem ext_iff {s t : set α} : s = t ↔ ∀ x, x ∈ s ↔ x ∈ t :=
 @[trans] theorem mem_of_mem_of_subset {x : α} {s t : set α}
   (hx : x ∈ s) (h : s ⊆ t) : x ∈ t := h hx
 
+lemma forall_in_swap {p : α → β → Prop} :
+  (∀ (a ∈ s) b, p a b) ↔ ∀ b (a ∈ s), p a b :=
+by tauto
+
 /-! ### Lemmas about `mem` and `set_of` -/
 
 @[simp] theorem mem_set_of_eq {a : α} {p : α → Prop} : a ∈ {a | p a} = p a := rfl

src/order/filter/basic.lean

@@ -179,6 +179,10 @@ begin
   { rintro ⟨u, huf, hPu, hQu⟩, exact ⟨⟨u, huf, hPu⟩, u, huf, hQu⟩ }
 end
 
+lemma forall_in_swap {β : Type*} {p : set α → β → Prop} :
+  (∀ (a ∈ f) b, p a b) ↔ ∀ b (a ∈ f), p a b :=
+set.forall_in_swap
+
 end filter
 
 namespace tactic.interactive

src/topology/uniform_space/uniform_convergence.lean

@@ -96,6 +96,11 @@ lemma tendsto_uniformly_iff_tendsto {F : ι → α → β} {f : α → β} {p :
   tendsto_uniformly F f p ↔ tendsto (λ q : ι × α, (f q.2, F q.1 q.2)) (p ×ᶠ ⊤) (𝓤 β) :=
 forall₂_congr $ λ u u_in, by simp [mem_map, filter.eventually, mem_prod_top]
 
+/-- Uniform converence implies pointwise convergence. -/
+lemma tendsto_uniformly.tendsto_at (h : tendsto_uniformly F f p) (x : α) :
+  tendsto (λ n, F n x) p $ 𝓝 (f x) :=
+uniform.tendsto_nhds_right.mpr $ λ u hu, mem_map.mpr $ by { filter_upwards [h u hu], tauto, }
+
 lemma tendsto_uniformly_on_univ :
   tendsto_uniformly_on F f p univ ↔ tendsto_uniformly F f p :=
 by simp [tendsto_uniformly_on, tendsto_uniformly]
@@ -277,6 +282,19 @@ begin
            ht₂.mono (λ i hi y hy, hi y hy.2 (hu₂ (by simp [hy.1])))⟩, },
 end
 
+lemma tendsto_locally_uniformly_iff_forall_tendsto :
+  tendsto_locally_uniformly F f p ↔
+  ∀ x, tendsto (λ (y : ι × α), (f y.2, F y.1 y.2)) (p ×ᶠ (𝓝 x)) (𝓤 β) :=
+begin
+  simp only [tendsto_locally_uniformly, filter.forall_in_swap, tendsto_def, mem_prod_iff,
+    set.prod_subset_iff],
+  refine forall₃_congr (λ x u hu, ⟨_, _⟩),
+  { rintros ⟨n, hn, hp⟩,
+    exact ⟨_, hp, n, hn, λ i hi a ha, hi a ha⟩, },
+  { rintros ⟨I, hI, n, hn, hu⟩,
+    exact ⟨n, hn, by filter_upwards [hI] using hu⟩, },
+end
+
 protected lemma tendsto_uniformly_on.tendsto_locally_uniformly_on
   (h : tendsto_uniformly_on F f p s) : tendsto_locally_uniformly_on F f p s :=
 λ u hu x hx, ⟨s, self_mem_nhds_within, h u hu⟩