obtain ⟨t, htf, ht⟩ := eventually_smallSets.mp hf.eventually_bddAbove
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : ℂ → β
x : ℂ
hf : Tendsto f (𝓝[≠] x) (𝓝 y)
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, BddAbove (f '' (Square x c \ {x}))
case intro.intro
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : ℂ → β
x : ℂ
hf : Tendsto f (𝓝[≠] x) (𝓝 y)
t : Set ℂ
htf : t ∈ 𝓝[≠] x
ht : ∀ t_1 ⊆ t, BddAbove (f '' t_1)
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, BddAbove (f '' (Square x c \ {x}))