∀ {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} [inst : TopologicalSpace α] [inst_1 : Zero β]
  [inst_2 : TopologicalSpace β] [inst_3 : FunLike F α β] [toContinuousMapClass : ContinuousMapClass F α β],
  (∀ (f : F), Filter.Tendsto (⇑f) (Filter.cocompact α) (nhds 0)) → ZeroAtInftyContinuousMapClass F α β