English
If an analytic function vanishes in a neighborhood of every point of a preconnected set, it is identically zero on the set.
Русский
Если аналитическая функция нулевая в окрестности каждой точки предсоединённого множества, она тождественно нулевая на этом множестве.
LaTeX
$$$\\text{AnalyticOnNhd } f U \\land \\text{IsPreconnected } U \\implies (f=0)\\text{ on } U.$$$
Lean4
/-- The *identity principle* for analytic functions: If two analytic functions coincide in a whole
neighborhood of a point `z₀`, then they coincide globally along a connected set.
For a one-dimensional version assuming only that the functions coincide at some points
arbitrarily close to `z₀`, see `AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq`. -/
theorem eqOn_of_preconnected_of_eventuallyEq {f g : E → F} {U : Set E} (hf : AnalyticOnNhd 𝕜 f U)
(hg : AnalyticOnNhd 𝕜 g U) (hU : IsPreconnected U) {z₀ : E} (h₀ : z₀ ∈ U) (hfg : f =ᶠ[𝓝 z₀] g) : EqOn f g U :=
by
have hfg' : f - g =ᶠ[𝓝 z₀] 0 := hfg.mono fun z h => by simp [h]
simpa [sub_eq_zero] using fun z hz => (hf.sub hg).eqOn_zero_of_preconnected_of_eventuallyEq_zero hU h₀ hfg' hz
