English
If f is analytic at x and not locally constant near x, then the image of punctured neighborhoods near x is contained in punctured neighborhoods near f(x).
Русский
Если f аналитична в окрестностях x и не локально постоянна, то образ punctured окрестностей около x содержится в punctured окрестностях около f(x).
LaTeX
$$$$\\text{If } f\\text{ is analytic at } x\\text{ and not locally constant, then }(\\mathcal{N}_{x}^{\\neq})\\!\\xrightarrow{f}\\! (\\mathcal{N}_{f(x)}^{\\neq}).$$$$
Lean4
/-- Preimages of codiscrete sets, local version: if `f` is analytic at `x` and not locally constant,
then the preimage of any punctured neighbourhood of `f x` is a punctured neighbourhood of `x`. -/
theorem preimage_of_nhdsNE {x : 𝕜} {f : 𝕜 → E} {s : Set E} (hfx : AnalyticAt 𝕜 f x) (h₂f : ¬EventuallyConst f (𝓝 x))
(hs : s ∈ 𝓝[≠] f x) : f ⁻¹' s ∈ 𝓝[≠] x :=
by
have : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s :=
by
filter_upwards [hfx.continuousAt.preimage_mem_nhds (insert_mem_nhds_iff.2 hs)]
tauto
contrapose! h₂f with h
rw [eventuallyConst_iff_exists_eventuallyEq]
use f x
rw [EventuallyEq, ← hfx.frequently_eq_iff_eventually_eq analyticAt_const]
apply ((frequently_imp_distrib_right.2 h).and_eventually (eventually_nhdsWithin_of_eventually_nhds this)).mono
intro z ⟨h₁z, h₂z⟩
rw [Set.mem_insert_iff] at h₂z
tauto
