∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_3} [inst_1 : TopologicalSpace Y] {f : OnePoint X → Y},
  ContinuousAt f OnePoint.infty ↔
    ∀ s ∈ nhds (f OnePoint.infty), ∃ t, IsClosed t ∧ IsCompact t ∧ Set.MapsTo (f ∘ OnePoint.some) tᶜ s