ι : Type u_1
κ : Type ?u.58187
X : Type u_2
Y : Type ?u.58193
Z : Type ?u.58196
α : Type u_3
β : Type ?u.58202
γ : Type ?u.58205
𝓕 : Type ?u.58208
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔
    ∀ (i : Set (α × α)),
      i ∈ 𝓤 α →
        ∀ᶠ (x : X) in 𝓝 x₀,
          (↑UniformFun.ofFun ∘ Function.swap F) x ∈
            {g | ((↑UniformFun.ofFun ∘ Function.swap F) x₀, g) ∈ UniformFun.gen ι α i}
ι : Type u_1
κ : Type ?u.58187
X : Type u_2
Y : Type ?u.58193
Z : Type ?u.58196
α : Type u_3
β : Type ?u.58202
γ : Type ?u.58205
𝓕 : Type ?u.58208
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔ ContinuousAt (↑UniformFun.ofFun ∘ Function.swap F) x₀
rw [ContinuousAt, (UniformFun.hasBasis_nhds ι α _).tendsto_right_iff]
no goals
ι : Type u_1
κ : Type ?u.58187
X : Type u_2
Y : Type ?u.58193
Z : Type ?u.58196
α : Type u_3
β : Type ?u.58202
γ : Type ?u.58205
𝓕 : Type ?u.58208
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔
    ∀ (i : Set (α × α)),
      i ∈ 𝓤 α →
        ∀ᶠ (x : X) in 𝓝 x₀,
          (↑UniformFun.ofFun ∘ Function.swap F) x ∈
            {g | ((↑UniformFun.ofFun ∘ Function.swap F) x₀, g) ∈ UniformFun.gen ι α i}
rfl