no goals
ι : Type u_1
κ : Type ?u.79183
X : Type u_2
Y : Type ?u.79189
Z : Type ?u.79192
α : Type u_3
β : Type ?u.79198
γ : Type ?u.79201
𝓕 : Type ?u.79204
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
⊢ Equicontinuous F ↔ Continuous (↑UniformFun.ofFun ∘ Function.swap F)
simp_rw [Equicontinuous, continuous_iff_continuousAt, equicontinuousAt_iff_continuousAt]