# Uniqueness principle for analytic functions #

We show that two analytic functions which coincide around a point coincide on whole connected sets, in AnalyticOn.eqOn_of_preconnected_of_eventuallyEq.

theorem AnalyticOn.eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {F : Type u_3} [NormedSpace ๐ F] [] {f : E โ F} {U : Set E} (hf : AnalyticOn ๐ f U) (hU : ) {zโ : E} (hโ : zโ โ U) (hfzโ : f =แถ [nhds zโ] 0) :
Set.EqOn f 0 U

If an analytic function vanishes around a point, then it is uniformly zero along a connected set. Superseded by eqOn_zero_of_preconnected_of_locally_zero which does not assume completeness of the target space.

theorem AnalyticOn.eqOn_zero_of_preconnected_of_eventuallyEq_zero {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {F : Type u_3} [NormedSpace ๐ F] {f : E โ F} {U : Set E} (hf : AnalyticOn ๐ f U) (hU : ) {zโ : E} (hโ : zโ โ U) (hfzโ : f =แถ [nhds zโ] 0) :
Set.EqOn f 0 U

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 eqOn_zero_of_preconnected_of_frequently_eq_zero.

theorem AnalyticOn.eqOn_of_preconnected_of_eventuallyEq {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {F : Type u_3} [NormedSpace ๐ F] {f : E โ F} {g : E โ F} {U : Set E} (hf : AnalyticOn ๐ f U) (hg : AnalyticOn ๐ g U) (hU : ) {zโ : E} (hโ : zโ โ U) (hfg : f =แถ [nhds zโ] g) :
Set.EqOn f g U

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 eqOn_of_preconnected_of_frequently_eq.

theorem AnalyticOn.eq_of_eventuallyEq {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {F : Type u_3} [NormedSpace ๐ F] {f : E โ F} {g : E โ F} (hf : AnalyticOn ๐ f Set.univ) (hg : AnalyticOn ๐ g Set.univ) {zโ : E} (hfg : f =แถ [nhds zโ] g) :
f = g

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 eq_of_frequently_eq.