ι : Type u_3
κ✝ : Type ?u.126986
X : Type ?u.126989
Y : Type ?u.126992
Z : Type ?u.126995
α : Type u_2
β : Type u_4
γ : Type ?u.127004
𝓕 : Type ?u.127007
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
⊢ (∀ (i : κ),
      p i →
        ∀ᶠ (x : β × β) in 𝓤 β,
          ((↑UniformFun.ofFun ∘ Function.swap F) x.fst, (↑UniformFun.ofFun ∘ Function.swap F) x.snd) ∈
            (UniformFun.gen ι α ∘ s) i) ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.fst, F i xy.snd) ∈ s k
ι : Type u_3
κ✝ : Type ?u.126986
X : Type ?u.126989
Y : Type ?u.126992
Z : Type ?u.126995
α : Type u_2
β : Type u_4
γ : Type ?u.127004
𝓕 : Type ?u.127007
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 ↔ ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.fst, F i xy.snd) ∈ s k
rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
  (UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff]
no goals
ι : Type u_3
κ✝ : Type ?u.126986
X : Type ?u.126989
Y : Type ?u.126992
Z : Type ?u.126995
α : Type u_2
β : Type u_4
γ : Type ?u.127004
𝓕 : Type ?u.127007
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
⊢ (∀ (i : κ),
      p i →
        ∀ᶠ (x : β × β) in 𝓤 β,
          ((↑UniformFun.ofFun ∘ Function.swap F) x.fst, (↑UniformFun.ofFun ∘ Function.swap F) x.snd) ∈
            (UniformFun.gen ι α ∘ s) i) ↔
    ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), (F i xy.fst, F i xy.snd) ∈ s k
rfl