no goals
ι : Type u_2
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
β : Type u_1
inst✝ : UniformSpace β
f : β → (i : ι) → α i
⊢ UniformContinuous f ↔ ∀ (i : ι), UniformContinuous fun x => f x i
simp only [UniformContinuous, Pi.uniformity, tendsto_iInf, tendsto_comap_iff, Function.comp]