ι : Type u_1
κ : Type ?u.49263
X : Type ?u.49266
Y : Type ?u.49269
Z : Type ?u.49272
α : Type u_2
β : Type u_3
γ : Type ?u.49281
𝓕 : Type ?u.49284
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → β → α
h : UniformEquicontinuous F
⊢ UniformEquicontinuous (F ∘ rangeSplitting F)
ι : Type u_1
κ : Type ?u.49263
X : Type ?u.49266
Y : Type ?u.49269
Z : Type ?u.49272
α : Type u_2
β : Type u_3
γ : Type ?u.49281
𝓕 : Type ?u.49284
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → β → α
h : UniformEquicontinuous F
⊢ UniformEquicontinuous Subtype.val
rw [← comp_rangeSplitting F]
no goals
ι : Type u_1
κ : Type ?u.49263
X : Type ?u.49266
Y : Type ?u.49269
Z : Type ?u.49272
α : Type u_2
β : Type u_3
γ : Type ?u.49281
𝓕 : Type ?u.49284
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → β → α
h : UniformEquicontinuous F
⊢ UniformEquicontinuous (F ∘ rangeSplitting F)
exact h.comp _