α : Type u_3
β : Type u_2
γ : Type ?u.48697
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_1
F : ι → β → α
inst✝ : CompactSpace β
h : Continuous (↑UniformFun.ofFun ∘ Function.swap F)
⊢ UniformEquicontinuous F
α : Type u_3
β : Type u_2
γ : Type ?u.48697
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_1
F : ι → β → α
inst✝ : CompactSpace β
h : Equicontinuous F
⊢ UniformEquicontinuous F
rw [equicontinuous_iff_continuous] at h
α : Type u_3
β : Type u_2
γ : Type ?u.48697
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_1
F : ι → β → α
inst✝ : CompactSpace β
h : Continuous (↑UniformFun.ofFun ∘ Function.swap F)
⊢ UniformContinuous (↑UniformFun.ofFun ∘ Function.swap F)
α : Type u_3
β : Type u_2
γ : Type ?u.48697
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_1
F : ι → β → α
inst✝ : CompactSpace β
h : Continuous (↑UniformFun.ofFun ∘ Function.swap F)
⊢ UniformEquicontinuous F
rw [uniformEquicontinuous_iff_uniformContinuous]
no goals
α : Type u_3
β : Type u_2
γ : Type ?u.48697
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_1
F : ι → β → α
inst✝ : CompactSpace β
h : Continuous (↑UniformFun.ofFun ∘ Function.swap F)
⊢ UniformContinuous (↑UniformFun.ofFun ∘ Function.swap F)
exact CompactSpace.uniformContinuous_of_continuous h