∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {l : Filter ι} [l.NeBot]
  {F : ι → β → α} {f : β → α} {S : Set β},
  (∀ x ∈ S, Filter.Tendsto (fun x_1 => F x_1 x) l (nhds (f x))) → UniformEquicontinuousOn F S → UniformContinuousOn f S