eventually_eq_or_eventually_ne — Mathlib

English

If a function f has two representations locally around z0 as z0-shifted powers times analytic nonvanishing factors, then the two exponents must coincide.

Русский

Если для f имеются две локальные представления вида z0-центрированной степени, умноженной на аналитическую не нулевую часть, то экспоненты совпадают.

LaTeX

$$$\forall m,n \; (\exists g, AnalyticAt g z_0 \wedge g(z_0) \neq 0 \wedge \forall z \approx z_0, f(z)=(z-z_0)^m g(z)) \Rightarrow (\exists g, AnalyticAt g z_0 \wedge g(z_0) \neq 0 \wedge \forall z \approx z_0, f(z)=(z-z_0)^n g(z)) \Rightarrow m=n$$$

Lean4

theorem eventually_eq_or_eventually_ne (hf : AnalyticAt 𝕜 f z₀) (hg : AnalyticAt 𝕜 g z₀) :
    (∀ᶠ z in 𝓝 z₀, f z = g z) ∨ ∀ᶠ z in 𝓝[≠] z₀, f z ≠ g z := by
  simpa [sub_eq_zero] using (hf.sub hg).eventually_eq_zero_or_eventually_ne_zero

Похожие утверждения