preimage_zero_mem_codiscrete — Mathlib

English

If an analytic f is not identically zero on the whole field, then the zeros set is codiscrete on the whole space.

Русский

Если аналитическая функция не тождественно нулевая на всей области, то множество её нулей кодискретно во всём пространстве.

LaTeX

$$preimage_zero_mem_codiscrete (AnalyticAt/AnalyticOnNhd on Set.univ) …$$

Lean4

/-- If an analytic function `f` is not constantly zero on `𝕜`, then its set of zeros is codiscrete.

See `AnalyticOnNhd.preimage_mem_codiscreteWithin` for a more general statement in preimages of
codiscrete sets.
-/
theorem preimage_zero_mem_codiscrete [ConnectedSpace 𝕜] {x : 𝕜} (hf : AnalyticOnNhd 𝕜 f Set.univ) (hx : f x ≠ 0) :
    f ⁻¹' {0}ᶜ ∈ codiscrete 𝕜 :=
  hf.preimage_zero_mem_codiscreteWithin hx trivial isConnected_univ

Похожие утверждения