English
If f and g are analytic on a connected domain and agree on a set accumulating at a point z0, then f and g are equal on the entire domain.
Русский
Если две функции аналитичны на связной области и совпадают на непрерывно накапливающемся множества, тогда они совпадают на всей области.
LaTeX
$$$$\\text{Let } f,g\\text{ be analytic on a connected set }U,\\; z_0\\in U.\\; \\\\ \\exists\\ as \\ z\\to z_0:\\ f(z)=g(z) \\text{ frequently }\\Rightarrow f=g \\text{ on } U.$$$$
Lean4
/-- The *identity principle* for analytic functions, global version: if two functions are
analytic on a connected set `U` and coincide at points which accumulate to a point `z₀ ∈ U`, then
they coincide globally in `U`.
For higher-dimensional versions requiring that the functions coincide in a neighborhood of `z₀`,
see `AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq`. -/
theorem eqOn_of_preconnected_of_frequently_eq (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U)
(hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfg : ∃ᶠ z in 𝓝[≠] z₀, f z = g z) : EqOn f g U :=
by
have hfg' : ∃ᶠ z in 𝓝[≠] z₀, (f - g) z = 0 := hfg.mono fun z h => by rw [Pi.sub_apply, h, sub_self]
simpa [sub_eq_zero] using fun z hz => (hf.sub hg).eqOn_zero_of_preconnected_of_frequently_eq_zero hU h₀ hfg' hz
