∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_3} [inst_1 : TopologicalSpace Y] [DiscreteTopology X]
  (f : OnePoint X → Y), Continuous f ↔ Filter.Tendsto (fun x => f ↑x) Filter.cofinite (nhds (f OnePoint.infty))