apply Filter.tendsto_add_atTop_nat
case a.refine'_3.convert_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => e + 2) Filter.atTop Filter.atTop
no goals