English
If two analytic functions on a normed space coincide in a neighborhood of a point z0, then they coincide everywhere on the space.
Русский
Если две аналитические функции на нормированном пространстве совпадают в окрестности точки z0, тогда они совпадают на всём пространстве.
LaTeX
$$$f,g:\\, E\\to F\\ \\text{analytic on }E:\\quad (\\exists x_0: z_0)\\; f|_{nhds(z_0)} = g|_{nhds(z_0)} \\Rightarrow f=g.$$$
Lean4
/-- The *identity principle* for analytic functions: If two analytic functions on a normed space
coincide in a neighborhood of a point `z₀`, then they coincide everywhere.
For a one-dimensional version assuming only that the functions coincide at some points
arbitrarily close to `z₀`, see `AnalyticOnNhd.eq_of_frequently_eq`. -/
theorem eq_of_eventuallyEq {f g : E → F} [PreconnectedSpace E] (hf : AnalyticOnNhd 𝕜 f univ)
(hg : AnalyticOnNhd 𝕜 g univ) {z₀ : E} (hfg : f =ᶠ[𝓝 z₀] g) : f = g :=
funext fun x => eqOn_of_preconnected_of_eventuallyEq hf hg isPreconnected_univ (mem_univ z₀) hfg (mem_univ x)
