ι : Type u_1
κ : Type ?u.31450
X : Type u_2
Y : Type ?u.31456
Z : Type ?u.31459
α : Type u_3
β : Type ?u.31465
γ : Type ?u.31468
𝓕 : Type ?u.31471
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
h : EquicontinuousAt F x₀
⊢ EquicontinuousAt (F ∘ rangeSplitting F) x₀
ι : Type u_1
κ : Type ?u.31450
X : Type u_2
Y : Type ?u.31456
Z : Type ?u.31459
α : Type u_3
β : Type ?u.31465
γ : Type ?u.31468
𝓕 : Type ?u.31471
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
h : EquicontinuousAt F x₀
⊢ EquicontinuousAt Subtype.val x₀
rw [← comp_rangeSplitting F]
no goals
ι : Type u_1
κ : Type ?u.31450
X : Type u_2
Y : Type ?u.31456
Z : Type ?u.31459
α : Type u_3
β : Type ?u.31465
γ : Type ?u.31468
𝓕 : Type ?u.31471
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
F : ι → X → α
x₀ : X
h : EquicontinuousAt F x₀
⊢ EquicontinuousAt (F ∘ rangeSplitting F) x₀
exact h.comp _