ι : Type u_3
κ✝ : Type ?u.122958
X : Type u_4
Y : Type ?u.122964
Z : Type ?u.122967
α : Type u_2
β : Type ?u.122973
γ : Type ?u.122976
𝓕 : Type ?u.122979
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_1
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
x₀ : X
hα : HasBasis (𝓤 α) p s
⊢ (∀ (i : κ),
      p i →
        ∀ᶠ (x : X) in 𝓝 x₀,
          (↑UniformFun.ofFun ∘ Function.swap F) x ∈
            {g | ((↑UniformFun.ofFun ∘ Function.swap F) x₀, g) ∈ UniformFun.gen ι α (s i)}) ↔
    ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k
ι : Type u_3
κ✝ : Type ?u.122958
X : Type u_4
Y : Type ?u.122964
Z : Type ?u.122967
α : Type u_2
β : Type ?u.122973
γ : Type ?u.122976
𝓕 : Type ?u.122979
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_1
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
x₀ : X
hα : HasBasis (𝓤 α) p s
⊢ EquicontinuousAt F x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k
rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
  (UniformFun.hasBasis_nhds_of_basis ι α _ hα).tendsto_right_iff]
no goals
ι : Type u_3
κ✝ : Type ?u.122958
X : Type u_4
Y : Type ?u.122964
Z : Type ?u.122967
α : Type u_2
β : Type ?u.122973
γ : Type ?u.122976
𝓕 : Type ?u.122979
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_1
p : κ → Prop
s : κ → Set (α × α)
F : ι → X → α
x₀ : X
hα : HasBasis (𝓤 α) p s
⊢ (∀ (i : κ),
      p i →
        ∀ᶠ (x : X) in 𝓝 x₀,
          (↑UniformFun.ofFun ∘ Function.swap F) x ∈
            {g | ((↑UniformFun.ofFun ∘ Function.swap F) x₀, g) ∈ UniformFun.gen ι α (s i)}) ↔
    ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k
rfl