BddAbove_on_rectangle_of_bdd_near

theorem BddAbove_on_rectangle_of_bdd_near {z w p : ℂ} {f : ℂ → ℂ}    (f_cont : ContinuousOn f (Rectangle z w \ {p}))    (f_near_p : f =O[𝓝[≠] p] (1 : ℂ → ℂ)) :    BddAbove (norm ∘ f '' (Rectangle z w \ {p})) := by  obtain ⟨V, V_in_nhds, V_prop⟩ := IsBigO_to_BddAbove f_near_p  rw [mem_nhds_iff] at V_in_nhds  obtain ⟨W, W_subset, W_open, p_in_W⟩ := V_in_nhds  set U := Rectangle z w  have : U \ {p} = (U \ W) ∪ ((U ∩ W) \ {p}) := by    ext x    simp only [Set.mem_sdiff, mem_singleton_iff, mem_union, mem_inter_iff]    constructor    · intro ⟨xu, x_not_p⟩      tauto    · intro h      rcases h with ⟨h1, h2⟩ | ⟨⟨h1, h2⟩, h3⟩      · refine ⟨h1, ?_⟩        intro h        rw [← h] at p_in_W        exact h2 p_in_W      · tauto  rw [this, image_union]  apply BddAbove.union  · apply IsCompact.bddAbove_image    · apply IsCompact.diff _ W_open      exact IsCompact.reProdIm isCompact_uIcc isCompact_uIcc    · apply f_cont.norm.mono      apply Set.sdiff_subset_sdiff_right      simpa  · exact V_prop.mono      (image_mono <| Set.sdiff_subset_sdiff_left <| subset_trans inter_subset_right W_subset)