Source indexedlemma · leanprover/lean4:v4.32.0

Perron.bddAbove_square_of_tendsto

PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:840 to 846

Mathematical statement

Exact Lean statement

lemma bddAbove_square_of_tendsto {f : ℂ → β} {x : ℂ}
    (hf : Tendsto f (𝓝[≠] x) (𝓝 y)) :
    ∀ᶠ (c : ℝ) in 𝓝[>] 0, BddAbove (f '' (Square x c \ {x}))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma bddAbove_square_of_tendsto {f : ℂ → β} {x : ℂ}    (hf : Tendsto f (𝓝[≠] x) (𝓝 y)) :    ∀ᶠ (c : ℝ) in 𝓝[>] 0, BddAbove (f '' (Square x c \ {x})) := by  obtain ⟨t, htf, ht⟩ := eventually_smallSets.mp hf.eventually_bddAbove  obtain ⟨ε, hε0, hε⟩ := nhdsWithin_hasBasis (nhds_hasBasis_square x) {x}ᶜ |>.1 t |>.mp htf  filter_upwards [Ioo_mem_nhdsGT hε0] with ε' ⟨hε'0, hε'⟩  exact ht _ <| (Set.sdiff_subset_sdiff (square_subset_square hε'0 hε'.le) subset_rfl).trans hε