no goals
ι : Type ?u.6949
α : Type ?u.6952
β : Type ?u.6955
l : Filter α
p : ℕ → Prop
⊢ (∃ᶠ (n : ℕ) in atTop, p n) ↔ Set.Infinite {n | p n}
rw [← Nat.cofinite_eq_atTop, frequently_cofinite_iff_infinite]