ι : Type u_3
κ✝ : Type ?u.121547
X : Type u_2
Y : Type ?u.121553
Z : Type ?u.121556
α : Type u_4
β : Type ?u.121562
γ : Type ?u.121565
𝓕 : Type ?u.121568
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_1
p : κ → Prop
s : κ → Set X
F : ι → X → α
x₀ : X
hX : HasBasis (𝓝 x₀) p s
⊢ (∀ (ib : Set (α × α)),
      ib ∈ 𝓤 α →
        ∃ ia,
          p ia ∧
            ∀ (x : X),
              x ∈ s ia →
                (↑UniformFun.ofFun ∘ Function.swap F) x ∈
                  {g | ((↑UniformFun.ofFun ∘ Function.swap F) x₀, g) ∈ UniformFun.gen ι α ib}) ↔
    ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ k, p k ∧ ∀ (x : X), x ∈ s k → ∀ (i : ι), (F i x₀, F i x) ∈ U
ι : Type u_3
κ✝ : Type ?u.121547
X : Type u_2
Y : Type ?u.121553
Z : Type ?u.121556
α : Type u_4
β : Type ?u.121562
γ : Type ?u.121565
𝓕 : Type ?u.121568
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_1
p : κ → Prop
s : κ → Set X
F : ι → X → α
x₀ : X
hX : HasBasis (𝓝 x₀) p s
⊢ EquicontinuousAt F x₀ ↔ ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ k, p k ∧ ∀ (x : X), x ∈ s k → ∀ (i : ι), (F i x₀, F i x) ∈ U
rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
  hX.tendsto_iff (UniformFun.hasBasis_nhds ι α _)]
ι : Type u_3
κ✝ : Type ?u.121547
X : Type u_2
Y : Type ?u.121553
Z : Type ?u.121556
α : Type u_4
β : Type ?u.121562
γ : Type ?u.121565
𝓕 : Type ?u.121568
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_1
p : κ → Prop
s : κ → Set X
F : ι → X → α
x₀ : X
hX : HasBasis (𝓝 x₀) p s
⊢ (∀ (ib : Set (α × α)),
      ib ∈ 𝓤 α →
        ∃ ia,
          p ia ∧
            ∀ (x : X),
              x ∈ s ia →
                (↑UniformFun.ofFun (Function.swap F x₀), ↑UniformFun.ofFun (Function.swap F x)) ∈
                  UniformFun.gen ι α ib) ↔
    ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ k, p k ∧ ∀ (x : X), x ∈ s k → ∀ (i : ι), (F i x₀, F i x) ∈ U
ι : Type u_3
κ✝ : Type ?u.121547
X : Type u_2
Y : Type ?u.121553
Z : Type ?u.121556
α : Type u_4
β : Type ?u.121562
γ : Type ?u.121565
𝓕 : Type ?u.121568
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_1
p : κ → Prop
s : κ → Set X
F : ι → X → α
x₀ : X
hX : HasBasis (𝓝 x₀) p s
⊢ (∀ (ib : Set (α × α)),
      ib ∈ 𝓤 α →
        ∃ ia,
          p ia ∧
            ∀ (x : X),
              x ∈ s ia →
                (↑UniformFun.ofFun ∘ Function.swap F) x ∈
                  {g | ((↑UniformFun.ofFun ∘ Function.swap F) x₀, g) ∈ UniformFun.gen ι α ib}) ↔
    ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ k, p k ∧ ∀ (x : X), x ∈ s k → ∀ (i : ι), (F i x₀, F i x) ∈ U
simp only [Function.comp_apply, mem_setOf_eq, exists_prop]
no goals
ι : Type u_3
κ✝ : Type ?u.121547
X : Type u_2
Y : Type ?u.121553
Z : Type ?u.121556
α : Type u_4
β : Type ?u.121562
γ : Type ?u.121565
𝓕 : Type ?u.121568
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_1
p : κ → Prop
s : κ → Set X
F : ι → X → α
x₀ : X
hX : HasBasis (𝓝 x₀) p s
⊢ (∀ (ib : Set (α × α)),
      ib ∈ 𝓤 α →
        ∃ ia,
          p ia ∧
            ∀ (x : X),
              x ∈ s ia →
                (↑UniformFun.ofFun (Function.swap F x₀), ↑UniformFun.ofFun (Function.swap F x)) ∈
                  UniformFun.gen ι α ib) ↔
    ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ k, p k ∧ ∀ (x : X), x ∈ s k → ∀ (i : ι), (F i x₀, F i x) ∈ U
rfl