ι : Type u_3
κ : Type ?u.130947
X : Type ?u.130950
Y : Type ?u.130953
Z : Type ?u.130956
α : Type u_1
β : Type u_4
γ : Type u_2
𝓕 : Type ?u.130968
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : UniformInducing u
this : UniformInducing (↑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ↑toFun)
⊢ UniformEquicontinuous F ↔ UniformEquicontinuous ((fun x x_1 => x ∘ x_1) u ∘ F)
ι : Type u_3
κ : Type ?u.130947
X : Type ?u.130950
Y : Type ?u.130953
Z : Type ?u.130956
α : Type u_1
β : Type u_4
γ : Type u_2
𝓕 : Type ?u.130968
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : UniformInducing u
⊢ UniformEquicontinuous F ↔ UniformEquicontinuous ((fun x x_1 => x ∘ x_1) u ∘ F)
have := UniformFun.postcomp_uniformInducing (α := ι) hu
ι : Type u_3
κ : Type ?u.130947
X : Type ?u.130950
Y : Type ?u.130953
Z : Type ?u.130956
α : Type u_1
β : Type u_4
γ : Type u_2
𝓕 : Type ?u.130968
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : UniformInducing u
this : UniformInducing (↑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ↑toFun)
⊢ UniformContinuous ((↑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ↑toFun) ∘ ↑UniformFun.ofFun ∘ Function.swap F) ↔
    UniformContinuous (↑UniformFun.ofFun ∘ Function.swap ((fun x x_1 => x ∘ x_1) u ∘ F))
ι : Type u_3
κ : Type ?u.130947
X : Type ?u.130950
Y : Type ?u.130953
Z : Type ?u.130956
α : Type u_1
β : Type u_4
γ : Type u_2
𝓕 : Type ?u.130968
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : UniformInducing u
this : UniformInducing (↑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ↑toFun)
⊢ UniformEquicontinuous F ↔ UniformEquicontinuous ((fun x x_1 => x ∘ x_1) u ∘ F)
rw [uniformEquicontinuous_iff_uniformContinuous, uniformEquicontinuous_iff_uniformContinuous,
  this.uniformContinuous_iff]
no goals
ι : Type u_3
κ : Type ?u.130947
X : Type ?u.130950
Y : Type ?u.130953
Z : Type ?u.130956
α : Type u_1
β : Type u_4
γ : Type u_2
𝓕 : Type ?u.130968
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : UniformInducing u
this : UniformInducing (↑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ↑toFun)
⊢ UniformContinuous ((↑UniformFun.ofFun ∘ (fun x => u ∘ x) ∘ ↑toFun) ∘ ↑UniformFun.ofFun ∘ Function.swap F) ↔
    UniformContinuous (↑UniformFun.ofFun ∘ Function.swap ((fun x x_1 => x ∘ x_1) u ∘ F))
rfl