Theorems · Theorem · complex analysis

AnalyticAt.preimage_of_nhdsNE

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E} {s : Set E},
  AnalyticAt 𝕜 f x → ¬Filter.EventuallyConst f (nhds x) → s ∈ nhdsWithin (f x) {f x}ᶜ → f ⁻¹' s ∈ nhdsWithin x {x}ᶜ

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.

Defined in

Mathlib.Analysis.Analytic.IsolatedZeros

Cited by

2 results in Mathlib

Foundations

Depth 192 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace