no goals
α : Type u_2
β : Type ?u.6300
ι : Type u_1
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
ha : IsLUB (range f) a
⊢ Tendsto f atBot (𝓝 a)
convert tendsto_atTop_isLUB h_anti.dual_left ha using 1