English
If f,g are analytic on a neighborhood of a preconnected set U and z0 ∈ U, and the set {z: f(z)=g(z)} accumulates at z0 within U, then f and g are equal on U.
Русский
Если f,g аналитичны в окрестности U, z0∈U и {z: f(z)=g(z)} накапливается в z0, то f=g на U.
LaTeX
$$$$\\text{Let } f,g\\text{ analytic on a neighborhood of }U, \\; z_0\\in U, \\\\ z_0\\ in\\ \\overline{\\{z: f(z)=g(z)\\}\\setminus\\{z_0\\}} \\Rightarrow f=g \\text{ on } U.$$$$
Lean4
/-- The *identity principle* for analytic functions, global version: if two functions on a normed
field `𝕜` are analytic everywhere and coincide at points which accumulate to a point `z₀`, then
they coincide globally.
For higher-dimensional versions requiring that the functions coincide in a neighborhood of `z₀`,
see `AnalyticOnNhd.eq_of_eventuallyEq`. -/
theorem eq_of_frequently_eq [ConnectedSpace 𝕜] (hf : AnalyticOnNhd 𝕜 f univ) (hg : AnalyticOnNhd 𝕜 g univ)
(hfg : ∃ᶠ z in 𝓝[≠] z₀, f z = g z) : f = g :=
funext fun x => eqOn_of_preconnected_of_frequently_eq hf hg isPreconnected_univ (mem_univ z₀) hfg (mem_univ x)
