sorry
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ interior s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
⊢ Filter.Tendsto (fun n => 1 / (↑n + 2)) Filter.atTop (nhds 0)
no goals