∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {ι : Type u₃} {p : Filter ι}
  {F : ι → C(α, β)} {f : C(α, β)},
  Filter.Tendsto F p (nhds f) = ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K