no goals
ι : Sort ?u.20384
α : Type u_2
β : Type u_1
X : Type ?u.20393
Y : Type ?u.20396
inst✝ : Preorder β
l : Filter α
f : α → Filter β
⊢ Tendsto f l (𝓝 atTop) ↔ ∀ (y : β), ∀ᶠ (a : α) in l, Ici y ∈ f a
simp only [nhds_atTop, tendsto_iInf, tendsto_principal, mem_Iic, le_principal_iff]