α : Type u_1
β : Type u_2
γ : Type ?u.44602
ι : Type ?u.44605
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
⊢ ∀ (i : α), UniformContinuous fun x => ↑toFun x i
α : Type u_1
β : Type u_2
γ : Type ?u.44602
ι : Type ?u.44605
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
⊢ UniformContinuous ↑toFun
rw [uniformContinuous_pi]
α : Type u_1
β : Type u_2
γ : Type ?u.44602
ι : Type ?u.44605
s s' : Set α
x✝ : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
x : α
⊢ UniformContinuous fun x_1 => ↑toFun x_1 x
α : Type u_1
β : Type u_2
γ : Type ?u.44602
ι : Type ?u.44605
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
⊢ ∀ (i : α), UniformContinuous fun x => ↑toFun x i
intro x
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.44602
ι : Type ?u.44605
s s' : Set α
x✝ : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
x : α
⊢ UniformContinuous fun x_1 => ↑toFun x_1 x
exact uniformContinuous_eval β x