no goals
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
f : Filter (OnePoint X)
⊢ f ≤ 𝓝 ∞ ↔ ∀ (s : Set X), IsClosed s → IsCompact s → some '' sᶜ ∪ {∞} ∈ f
simp only [hasBasis_nhds_infty.ge_iff, and_imp]