ι : Type u_3
κ✝ : Type ?u.125171
X : Type ?u.125174
Y : Type ?u.125177
Z : Type ?u.125180
α : Type u_4
β : Type u_2
γ : Type ?u.125189
𝓕 : Type ?u.125192
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_1
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
hβ : HasBasis (𝓤 β) p s
⊢ (∀ (ib : Set (α × α)),
      ib ∈ 𝓤 α →
        ∃ ia,
          p ia ∧
            ∀ (x : β × β),
              x ∈ s ia →
                ((↑UniformFun.ofFun ∘ Function.swap F) x.fst, (↑UniformFun.ofFun ∘ Function.swap F) x.snd) ∈
                  UniformFun.gen ι α ib) ↔
    ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
ι : Type u_3
κ✝ : Type ?u.125171
X : Type ?u.125174
Y : Type ?u.125177
Z : Type ?u.125180
α : Type u_4
β : Type u_2
γ : Type ?u.125189
𝓕 : Type ?u.125192
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_1
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
hβ : HasBasis (𝓤 β) p s
⊢ UniformEquicontinuous F ↔
    ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
  hβ.tendsto_iff (UniformFun.hasBasis_uniformity ι α)]
ι : Type u_3
κ✝ : Type ?u.125171
X : Type ?u.125174
Y : Type ?u.125177
Z : Type ?u.125180
α : Type u_4
β : Type u_2
γ : Type ?u.125189
𝓕 : Type ?u.125192
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_1
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
hβ : HasBasis (𝓤 β) p s
⊢ (∀ (ib : Set (α × α)),
      ib ∈ 𝓤 α →
        ∃ ia,
          p ia ∧
            ∀ (a b : β),
              (a, b) ∈ s ia →
                (↑UniformFun.ofFun (Function.swap F a), ↑UniformFun.ofFun (Function.swap F b)) ∈
                  UniformFun.gen ι α ib) ↔
    ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
ι : Type u_3
κ✝ : Type ?u.125171
X : Type ?u.125174
Y : Type ?u.125177
Z : Type ?u.125180
α : Type u_4
β : Type u_2
γ : Type ?u.125189
𝓕 : Type ?u.125192
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_1
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
hβ : HasBasis (𝓤 β) p s
⊢ (∀ (ib : Set (α × α)),
      ib ∈ 𝓤 α →
        ∃ ia,
          p ia ∧
            ∀ (x : β × β),
              x ∈ s ia →
                ((↑UniformFun.ofFun ∘ Function.swap F) x.fst, (↑UniformFun.ofFun ∘ Function.swap F) x.snd) ∈
                  UniformFun.gen ι α ib) ↔
    ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
simp only [Prod.forall, Function.comp_apply, mem_setOf_eq, exists_prop]
no goals
ι : Type u_3
κ✝ : Type ?u.125171
X : Type ?u.125174
Y : Type ?u.125177
Z : Type ?u.125180
α : Type u_4
β : Type u_2
γ : Type ?u.125189
𝓕 : Type ?u.125192
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ : Type u_1
p : κ → Prop
s : κ → Set (β × β)
F : ι → β → α
hβ : HasBasis (𝓤 β) p s
⊢ (∀ (ib : Set (α × α)),
      ib ∈ 𝓤 α →
        ∃ ia,
          p ia ∧
            ∀ (a b : β),
              (a, b) ∈ s ia →
                (↑UniformFun.ofFun (Function.swap F a), ↑UniformFun.ofFun (Function.swap F b)) ∈
                  UniformFun.gen ι α ib) ↔
    ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
rfl