Theorems · Theorem · complex analysis

AnalyticOnNhd.eq_of_frequently_eq

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} [ConnectedSpace 𝕜],
  AnalyticOnNhd 𝕜 f Set.univ → AnalyticOnNhd 𝕜 g Set.univ → (∃ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z = g z) → f = g

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.

Defined in

Mathlib.Analysis.Analytic.IsolatedZeros

Cited by

1 results in Mathlib

Foundations

Depth 193 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceConnectedSpace