eqOn_of_preconnected_of_mem_closure

English

If f,g are analytic on nhds of U and there is frequent equality of f and g near z0 (z0∈U) away from z0 itself, then f and g coincide on U.

Русский

Если f,g аналитичны на nhds(U) и существует частое совпадение f(z)=g(z) близко z0 (z0∈U) вне z0, то f≡g на U.

LaTeX

$$$$\\text{If } f,g\\text{ analytic on }U, \\; z_0\\in U, \\\\ \\text{Frequent}(z\\mapsto f(z)=g(z))\\text{ in }\\nhds(z_0) \\Rightarrow f=g \\text{ on }U.$$$$

Lean4

theorem eqOn_of_preconnected_of_mem_closure (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U)
    (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfg : z₀ ∈ closure ({z | f z = g z} \ { z₀ })) : EqOn f g U :=
  hf.eqOn_of_preconnected_of_frequently_eq hg hU h₀ (mem_closure_ne_iff_frequently_within.mp hfg)

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