[GOAL]
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
β : Type u_2
inst✝ : UniformSpace β
f : β → (i : ι) → α i
⊢ UniformContinuous f ↔ ∀ (i : ι), UniformContinuous fun x => f x i
[PROOFSTEP]
simp only [UniformContinuous, Pi.uniformity, tendsto_iInf, tendsto_comap_iff, Function.comp]
[GOAL]
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : ∀ (i : ι), CompleteSpace (α i)
⊢ ∀ {f : Filter ((i : ι) → α i)}, Cauchy f → ∃ x, f ≤ 𝓝 x
[PROOFSTEP]
intro f hf
[GOAL]
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : ∀ (i : ι), CompleteSpace (α i)
f : Filter ((i : ι) → α i)
hf : Cauchy f
⊢ ∃ x, f ≤ 𝓝 x
[PROOFSTEP]
haveI := hf.1
[GOAL]
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : ∀ (i : ι), CompleteSpace (α i)
f : Filter ((i : ι) → α i)
hf : Cauchy f
this : NeBot f
⊢ ∃ x, f ≤ 𝓝 x
[PROOFSTEP]
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
[GOAL]
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : ∀ (i : ι), CompleteSpace (α i)
f : Filter ((i : ι) → α i)
hf : Cauchy f
this : NeBot f
⊢ ∀ (i : ι), ∃ x, map (fun a => a i) f ≤ 𝓝 x
[PROOFSTEP]
intro i
[GOAL]
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : ∀ (i : ι), CompleteSpace (α i)
f : Filter ((i : ι) → α i)
hf : Cauchy f
this : NeBot f
i : ι
⊢ ∃ x, map (fun a => a i) f ≤ 𝓝 x
[PROOFSTEP]
have key : Cauchy (map (fun a : ∀ i : ι, α i => a i) f) := hf.map (Pi.uniformContinuous_proj α i)
[GOAL]
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : ∀ (i : ι), CompleteSpace (α i)
f : Filter ((i : ι) → α i)
hf : Cauchy f
this : NeBot f
i : ι
key : Cauchy (map (fun a => a i) f)
⊢ ∃ x, map (fun a => a i) f ≤ 𝓝 x
[PROOFSTEP]
exact cauchy_iff_exists_le_nhds.1 key
[GOAL]
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : ∀ (i : ι), CompleteSpace (α i)
f : Filter ((i : ι) → α i)
hf : Cauchy f
this✝ : NeBot f
this : ∀ (i : ι), ∃ x, map (fun a => a i) f ≤ 𝓝 x
⊢ ∃ x, f ≤ 𝓝 x
[PROOFSTEP]
choose x hx using this
[GOAL]
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : ∀ (i : ι), CompleteSpace (α i)
f : Filter ((i : ι) → α i)
hf : Cauchy f
this : NeBot f
x : (i : ι) → α i
hx : ∀ (i : ι), map (fun a => a i) f ≤ 𝓝 (x i)
⊢ ∃ x, f ≤ 𝓝 x
[PROOFSTEP]
use x
[GOAL]
case h
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : ∀ (i : ι), CompleteSpace (α i)
f : Filter ((i : ι) → α i)
hf : Cauchy f
this : NeBot f
x : (i : ι) → α i
hx : ∀ (i : ι), map (fun a => a i) f ≤ 𝓝 (x i)
⊢ f ≤ 𝓝 x
[PROOFSTEP]
rwa [nhds_pi, le_pi]
[GOAL]
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : ∀ (i : ι), SeparatedSpace (α i)
x y : (i : ι) → α i
H : ∀ (r : Set (((i : ι) → α i) × ((i : ι) → α i))), r ∈ 𝓤 ((i : ι) → α i) → (x, y) ∈ r
⊢ x = y
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : ∀ (i : ι), SeparatedSpace (α i)
x y : (i : ι) → α i
H : ∀ (r : Set (((i : ι) → α i) × ((i : ι) → α i))), r ∈ 𝓤 ((i : ι) → α i) → (x, y) ∈ r
i : ι
⊢ x i = y i
[PROOFSTEP]
apply eq_of_separated_of_uniformContinuous (Pi.uniformContinuous_proj α i)
[GOAL]
case h
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : ∀ (i : ι), SeparatedSpace (α i)
x y : (i : ι) → α i
H : ∀ (r : Set (((i : ι) → α i) × ((i : ι) → α i))), r ∈ 𝓤 ((i : ι) → α i) → (x, y) ∈ r
i : ι
⊢ (fun i => x i) ≈ fun i => y i
[PROOFSTEP]
apply H
