no goals
α : Type u_1
β : Type ?u.6026
ι : Sort ?u.6029
l l' la : Filter α
lb : Filter β
p : α → Prop
⊢ (∀ᶠ (s : Set α) in smallSets l, ∀ (x : α), x ∈ s → p x) ↔ ∀ᶠ (x : α) in l, p x
simpa only [inf_top_eq, eventually_top] using @eventually_smallSets_eventually α l ⊤ p