ι : Type u_1
κ : Type ?u.100604
X : Type ?u.100607
Y : Type ?u.100610
Z : Type ?u.100613
α : Type u_2
β : Type u_3
γ : Type ?u.100622
𝓕 : Type ?u.100625
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → β → α
⊢ UniformEquicontinuous F ↔
    ∀ (i : Set (α × α)),
      i ∈ 𝓤 α →
        ∀ᶠ (x : β × β) in 𝓤 β,
          ((↑UniformFun.ofFun ∘ Function.swap F) x.fst, (↑UniformFun.ofFun ∘ Function.swap F) x.snd) ∈
            UniformFun.gen ι α i
ι : Type u_1
κ : Type ?u.100604
X : Type ?u.100607
Y : Type ?u.100610
Z : Type ?u.100613
α : Type u_2
β : Type u_3
γ : Type ?u.100622
𝓕 : Type ?u.100625
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → β → α
⊢ UniformEquicontinuous F ↔ UniformContinuous (↑UniformFun.ofFun ∘ Function.swap F)
rw [UniformContinuous, (UniformFun.hasBasis_uniformity ι α).tendsto_right_iff]
no goals
ι : Type u_1
κ : Type ?u.100604
X : Type ?u.100607
Y : Type ?u.100610
Z : Type ?u.100613
α : Type u_2
β : Type u_3
γ : Type ?u.100622
𝓕 : Type ?u.100625
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → β → α
⊢ UniformEquicontinuous F ↔
    ∀ (i : Set (α × α)),
      i ∈ 𝓤 α →
        ∀ᶠ (x : β × β) in 𝓤 β,
          ((↑UniformFun.ofFun ∘ Function.swap F) x.fst, (↑UniformFun.ofFun ∘ Function.swap F) x.snd) ∈
            UniformFun.gen ι α i
rfl