ι : Type u_3
κ : Type ?u.129520
X : Type u_4
Y : Type ?u.129526
Z : Type ?u.129529
α : Type u_1
β : Type u_2
γ : Type ?u.129538
𝓕 : Type ?u.129541
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
u : α → β
hu : UniformInducing u
this : Inducing (↑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ↑toFun)
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x x_1 => x ∘ x_1) u ∘ F) x₀
ι : Type u_3
κ : Type ?u.129520
X : Type u_4
Y : Type ?u.129526
Z : Type ?u.129529
α : Type u_1
β : Type u_2
γ : Type ?u.129538
𝓕 : Type ?u.129541
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
u : α → β
hu : UniformInducing u
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x x_1 => x ∘ x_1) u ∘ F) x₀
have := (UniformFun.postcomp_uniformInducing (α := ι) hu).inducing
ι : Type u_3
κ : Type ?u.129520
X : Type u_4
Y : Type ?u.129526
Z : Type ?u.129529
α : Type u_1
β : Type u_2
γ : Type ?u.129538
𝓕 : Type ?u.129541
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
u : α → β
hu : UniformInducing u
this : Inducing (↑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ↑toFun)
⊢ ContinuousAt ((↑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ↑toFun) ∘ ↑UniformFun.ofFun ∘ Function.swap F) x₀ ↔
    ContinuousAt (↑UniformFun.ofFun ∘ Function.swap ((fun x x_1 => x ∘ x_1) u ∘ F)) x₀
ι : Type u_3
κ : Type ?u.129520
X : Type u_4
Y : Type ?u.129526
Z : Type ?u.129529
α : Type u_1
β : Type u_2
γ : Type ?u.129538
𝓕 : Type ?u.129541
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
u : α → β
hu : UniformInducing u
this : Inducing (↑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ↑toFun)
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x x_1 => x ∘ x_1) u ∘ F) x₀
rw [equicontinuousAt_iff_continuousAt, equicontinuousAt_iff_continuousAt, this.continuousAt_iff]
no goals
ι : Type u_3
κ : Type ?u.129520
X : Type u_4
Y : Type ?u.129526
Z : Type ?u.129529
α : Type u_1
β : Type u_2
γ : Type ?u.129538
𝓕 : Type ?u.129541
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
u : α → β
hu : UniformInducing u
this : Inducing (↑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ↑toFun)
⊢ ContinuousAt ((↑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ↑toFun) ∘ ↑UniformFun.ofFun ∘ Function.swap F) x₀ ↔
    ContinuousAt (↑UniformFun.ofFun ∘ Function.swap ((fun x x_1 => x ∘ x_1) u ∘ F)) x₀
rfl