English
Under completeness, if an analytic function vanishes near z0 and U is preconnected, then it is identically zero on U.
Русский
При полноте пространства и если аналитическая функция нулeвая в окрестности z0 и U предсоединено, то она нулeвая на всём U.
LaTeX
$$$\\text{EqOn } f 0 U$ при условии $\\text{AnalyticOnNhd } f U$, $U$ предсоединено и $z_0\\in U$ и $f=0$ в окрестности $z_0$.$$
Lean4
/-- The *identity principle* for analytic functions: If an analytic function vanishes in a whole
neighborhood of a point `z₀`, then it is uniformly zero along a connected set. For a one-dimensional
version assuming only that the function vanishes at some points arbitrarily close to `z₀`, see
`AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero`. -/
theorem eqOn_zero_of_preconnected_of_eventuallyEq_zero {f : E → F} {U : Set E} (hf : AnalyticOnNhd 𝕜 f U)
(hU : IsPreconnected U) {z₀ : E} (h₀ : z₀ ∈ U) (hfz₀ : f =ᶠ[𝓝 z₀] 0) : EqOn f 0 U :=
by
let F' := UniformSpace.Completion F
set e : F →L[𝕜] F' := UniformSpace.Completion.toComplL
have : AnalyticOnNhd 𝕜 (e ∘ f) U := fun x hx => (e.analyticAt _).comp (hf x hx)
have A : EqOn (e ∘ f) 0 U :=
by
apply eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux this hU h₀
filter_upwards [hfz₀] with x hx
simp only [hx, Function.comp_apply, Pi.zero_apply, map_zero]
intro z hz
have : e (f z) = e 0 := by simpa only using A hz
exact UniformSpace.Completion.coe_injective F this
