BddAbove_to_IsBigO

@[blueprint  (title := "BddAbove-to-IsBigO")  (statement := /--  If $f$ is bounded above in a punctured neighborhood of $p$, then $f$ is $O(1)$ in that  neighborhood.  -/)  (proof := /-- Elementary. -/)]lemma BddAbove_to_IsBigO {f : ℂ → ℂ} {p : ℂ}    {U : Set ℂ} (hU : U ∈ 𝓝 p) (bdd : BddAbove (norm ∘ f '' (U \ {p}))) :    f =O[𝓝[≠] p] (1 : ℂ → ℂ)  := by  dsimp [BddAbove, upperBounds] at bdd  rcases bdd with ⟨C, hC⟩   have h : ∀ x ∈ U \ {p}, ‖f x‖ ≤ C := by    intro x hx    have fx_is_norm : ‖f x‖ ∈ norm ∘ f ''(U \ {p}) := by      exact ⟨x, hx, rfl⟩    exact hC fx_is_norm   rw [Asymptotics.isBigO_iff]  use C  rw [eventually_nhdsWithin_iff]  simp only [Set.mem_sdiff, mem_singleton_iff, and_imp, mem_compl_iff, Pi.one_apply, one_mem,    CStarRing.norm_of_mem_unitary, mul_one] at h ⊢  filter_upwards [hU] using h