feat(topology/uniform_space/uniform_convergence): Product of `tendsto…

…_uniformly` (#11562)

This PR adds lemmas `tendsto_uniformly_on.prod` and `tendsto_uniformly.prod`.



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

src/topology/uniform_space/uniform_convergence.lean

@@ -129,6 +129,37 @@ lemma tendsto_uniformly.comp' [uniform_space γ] {g : β → γ} (h : tendsto_un
   (hg : uniform_continuous g) : tendsto_uniformly (λ i, g ∘ (F i)) (g ∘ f) p :=
 λ u hu, h _ (hg hu)
 
+lemma tendsto_uniformly_on.prod_map {ι' α' β' : Type*} [uniform_space β']
+  {F' : ι' → α' → β'} {f' : α' → β'} {p' : filter ι'} {s' : set α'}
+  (h : tendsto_uniformly_on F f p s) (h' : tendsto_uniformly_on F' f' p' s') :
+  tendsto_uniformly_on (λ (i : ι × ι'), prod.map (F i.1) (F' i.2))
+    (prod.map f f') (p.prod p') (s ×ˢ s') :=
+begin
+  intros u hu,
+  rw [uniformity_prod_eq_prod, mem_map, mem_prod_iff] at hu,
+  obtain ⟨v, hv, w, hw, hvw⟩ := hu,
+  exact mem_prod_iff.mpr ⟨_, h v hv, _, h' w hw,
+    λ i hi a ha, hvw (show (_, _) ∈ v ×ˢ w, from ⟨hi.1 a.1 ha.1, hi.2 a.2 ha.2⟩)⟩,
+end
+
+lemma tendsto_uniformly.prod_map {ι' α' β' : Type*} [uniform_space β'] {F' : ι' → α' → β'}
+  {f' : α' → β'} {p' : filter ι'} (h : tendsto_uniformly F f p) (h' : tendsto_uniformly F' f' p') :
+  tendsto_uniformly (λ (i : ι × ι'), prod.map (F i.1) (F' i.2)) (prod.map f f') (p.prod p') :=
+begin
+  rw [←tendsto_uniformly_on_univ, ←univ_prod_univ] at *,
+  exact h.prod_map h',
+end
+
+lemma tendsto_uniformly_on.prod {ι' β' : Type*} [uniform_space β'] {F' : ι' → α → β'} {f' : α → β'}
+  {p' : filter ι'} (h : tendsto_uniformly_on F f p s) (h' : tendsto_uniformly_on F' f' p' s) :
+  tendsto_uniformly_on (λ (i : ι × ι') a, (F i.1 a, F' i.2 a)) (λ a, (f a, f' a)) (p.prod p') s :=
+(congr_arg _ s.inter_self).mp ((h.prod_map h').comp (λ a, (a, a)))
+
+lemma tendsto_uniformly.prod {ι' β' : Type*} [uniform_space β'] {F' : ι' → α → β'} {f' : α → β'}
+  {p' : filter ι'} (h : tendsto_uniformly F f p) (h' : tendsto_uniformly F' f' p') :
+  tendsto_uniformly (λ (i : ι × ι') a, (F i.1 a, F' i.2 a)) (λ a, (f a, f' a)) (p.prod p') :=
+(h.prod_map h').comp (λ a, (a, a))
+
 /-- Uniform convergence to a constant function is equivalent to convergence in `p ×ᶠ ⊤`. -/
 lemma tendsto_prod_top_iff {c : β} : tendsto ↿F (p ×ᶠ ⊤) (𝓝 c) ↔ tendsto_uniformly F (λ _, c) p :=
 let j : β → β × β := prod.mk c in