feat: Port/Topology.UniformSpace.Pi (#2048)

port of topology.uniform_space.pi

all simple fixes

Mathlib.lean

@@ -986,6 +986,7 @@ import Mathlib.Topology.SubsetProperties
 import Mathlib.Topology.Support
 import Mathlib.Topology.UniformSpace.Basic
 import Mathlib.Topology.UniformSpace.Cauchy
+import Mathlib.Topology.UniformSpace.Pi
 import Mathlib.Topology.UniformSpace.Separation
 import Mathlib.Util.AtomM
 import Mathlib.Util.Export

Mathlib/Topology/UniformSpace/Pi.lean

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2019 Patrick Massot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Patrick Massot
+
+! This file was ported from Lean 3 source module topology.uniform_space.pi
+! leanprover-community/mathlib commit 2705404e701abc6b3127da906f40bae062a169c9
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Topology.UniformSpace.Cauchy
+import Mathlib.Topology.UniformSpace.Separation
+
+/-!
+# Indexed product of uniform spaces
+-/
+
+
+noncomputable section
+
+open Uniformity Topology
+
+section
+
+open Filter UniformSpace
+
+universe u
+
+variable {ι : Type _} (α : ι → Type u) [U : ∀ i, UniformSpace (α i)]
+
+
+instance Pi.uniformSpace : UniformSpace (∀ i, α i) :=
+  UniformSpace.ofCoreEq (⨅ i, UniformSpace.comap (fun a : ∀ i, α i => a i) (U i)).toCore
+      Pi.topologicalSpace <|
+    Eq.symm toTopologicalSpace_infᵢ
+#align Pi.uniform_space Pi.uniformSpace
+
+theorem Pi.uniformity : 𝓤 (∀ i, α i) = ⨅ i : ι, (Filter.comap fun a => (a.1 i, a.2 i)) <| 𝓤 (α i) :=
+  infᵢ_uniformity
+#align Pi.uniformity Pi.uniformity
+
+variable {α}
+
+theorem uniformContinuous_pi {β : Type _} [UniformSpace β] {f : β → ∀ i, α i} :
+    UniformContinuous f ↔ ∀ i, UniformContinuous fun x => f x i := by
+  -- porting note: required `Function.comp` to close
+  simp only [UniformContinuous, Pi.uniformity, tendsto_infᵢ, tendsto_comap_iff, Function.comp]
+#align uniform_continuous_pi uniformContinuous_pi
+
+variable (α)
+
+theorem Pi.uniformContinuous_proj (i : ι) : UniformContinuous fun a : ∀ i : ι, α i => a i :=
+  uniformContinuous_pi.1 uniformContinuous_id i
+#align Pi.uniform_continuous_proj Pi.uniformContinuous_proj
+
+instance Pi.complete [∀ i, CompleteSpace (α i)] : CompleteSpace (∀ i, α i) :=
+  ⟨by
+    intro f hf
+    haveI := hf.1
+    have : ∀ i, ∃ x : α i, Filter.map (fun a : ∀ i, α i => a i) f ≤ 𝓝 x :=
+      by
+      intro i
+      have key : Cauchy (map (fun a : ∀ i : ι, α i => a i) f) :=
+        hf.map (Pi.uniformContinuous_proj α i)
+      exact cauchy_iff_exists_le_nhds.1 key
+    choose x hx using this
+    use x
+    rwa [nhds_pi, le_pi]⟩
+#align Pi.complete Pi.complete
+
+instance Pi.separated [∀ i, SeparatedSpace (α i)] : SeparatedSpace (∀ i, α i) :=
+  separated_def.2 fun x y H => by
+    ext i
+    -- porting note: should be `eq_ofSeparated_ofUniformContinuous`?
+    apply eq_of_separated_of_uniformContinuous (Pi.uniformContinuous_proj α i)
+    apply H
+#align Pi.separated Pi.separated
+
+end