∀ {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {H : Set (X → α)} {S : Set X} {x₀ : X},
  H.EquicontinuousWithinAt S x₀ → ∀ {f : X → α}, f ∈ H → ContinuousWithinAt f S x₀