English
If f is analytic on nhd U, f x ≠ 0, x ∈ U and U is connected, then the set where f ≠ 0 is codiscreteWithin U.
Русский
Если f аналитична на граничной окрестности U, f(x) ≠ 0, x ∈ U и U связано, то множество точек, где f ≠ 0, кодискретно внутри U.
LaTeX
$$$f^{-1}\{0}^c \in codiscreteWithin\, U$ under the given hypotheses$$
Lean4
/-- If an analytic function `f` is not constantly zero on a connected set `U`, then its set of zeros is
codiscrete within `U`.
See `AnalyticOnNhd.preimage_mem_codiscreteWithin` for a more general statement in preimages of
codiscrete sets.
-/
theorem preimage_zero_mem_codiscreteWithin {x : 𝕜} (h₁f : AnalyticOnNhd 𝕜 f U) (h₂f : f x ≠ 0) (hx : x ∈ U)
(hU : IsConnected U) : f ⁻¹' {0}ᶜ ∈ codiscreteWithin U :=
by
filter_upwards [h₁f.codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_top, self_mem_codiscreteWithin U] with a ha h₂a
rw [← (h₁f x hx).analyticOrderAt_eq_zero] at h₂f
have {u : U} : analyticOrderAt f u ≠ ⊤ :=
by
apply (h₁f.exists_analyticOrderAt_ne_top_iff_forall hU).1
use ⟨x, hx⟩
simp_all
simp_all [(h₁f a h₂a).analyticOrderAt_eq_zero]
