no goals
α : Type u_2
β : Type ?u.27589
ι : Type u_1
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : InfConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
hbdd : BddBelow (range f)
⊢ Tendsto f atTop (𝓝 (⨅ (i : ι), f i))
convert tendsto_atBot_ciSup h_anti.dual hbdd.dual using 1