eqOn_zero_of_preconnected_of_mem_closure

English

If f is analytic on a nhd of U and z0 ∈ U, and z0 lies in the closure of {z: f(z) = 0} minus z0, then f is identically zero on U.

Русский

Пусть f аналитична в окрестности U и z0∈U; если z0 принадлежит замыканию множества {z: f(z) = 0} без точки z0, то f равна нулю на всём U.

LaTeX

$$$$\\text{Let } f \\text{ be analytic on a neighborhood of } U, \\; z_0 \\in U. \\\\ z_0 \\in \\overline{\\{z:\\ f(z)=0\\}\\setminus\\{z_0\\}} \\quad \\Longrightarrow \\quad f|_U \\equiv 0.$$$$

Lean4

theorem eqOn_zero_of_preconnected_of_mem_closure (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) (h₀ : z₀ ∈ U)
    (hfz₀ : z₀ ∈ closure ({z | f z = 0} \ { z₀ })) : EqOn f 0 U :=
  hf.eqOn_zero_of_preconnected_of_frequently_eq_zero hU h₀ (mem_closure_ne_iff_frequently_within.mp hfz₀)

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