English
For analytic f at z0, the existence of a representation f(z)=(z−z0)^n g(z) with analytic nonvanishing g is equivalent to the negation of a universal local zero condition.
Русский
Для аналитической f в z0 наличие представления f(z)=(z−z0)^n g(z) с аналитически не нулевым g эквивалентно не выполнению всеобъемлющего локального нулевого условия.
LaTeX
$$$AnalyticAt f z0 \Rightarrow (\exists n,g, AnalyticAt g z0 \wedge g z0 \neq 0 \wedge \forall^\! z near z0, f z = (z-z0)^n g z) \Leftrightarrow \neg \forall^\! z near z0, f z = 0$$$
Lean4
/-- The *principle of isolated zeros* for an analytic function, global version: if a function is
analytic on a connected set `U` and vanishes in arbitrary neighborhoods of a point `z₀ ∈ U`, then
it is identically zero in `U`.
For higher-dimensional versions requiring that the function vanishes in a neighborhood of `z₀`,
see `AnalyticOnNhd.eqOn_zero_of_preconnected_of_eventuallyEq_zero`. -/
theorem eqOn_zero_of_preconnected_of_frequently_eq_zero (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) (h₀ : z₀ ∈ U)
(hfw : ∃ᶠ z in 𝓝[≠] z₀, f z = 0) : EqOn f 0 U :=
hf.eqOn_zero_of_preconnected_of_eventuallyEq_zero hU h₀ ((hf z₀ h₀).frequently_zero_iff_eventually_zero.1 hfw)
