Theorems · Theorem · complex analysis

AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq

• 1000+ list: Identity theorem

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

The identity principle for analytic functions, global version: if two functions are analytic on a connected set U and coincide at points which accumulate to a point z₀ ∈ U, then they coincide globally in U. For higher-dimensional versions requiring that the functions coincide in a neighborhood of z₀, see AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq.

Defined in

Mathlib.Analysis.Analytic.IsolatedZeros

Cited by

4 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace