eq_zero_of_eventually — Mathlib

English

If hp and hq hold HasFPowerSeriesAt for two representations and the two base functions agree eventually near x, then p = q.

Русский

Если hp и hq задают два представления, и основания функций сходятся на окрестности x, то p = q.

LaTeX

$$$\\text{HasFPowerSeriesAt}\\, f\\, p\\, x \\rightarrow \\text{HasFPowerSeriesAt}\\, g\\, q\\, x \\rightarrow f = g\\text{ in a neighborhood of } x \\Rightarrow p=q.$$$

Lean4

/-- A one-dimensional formal multilinear series representing a locally zero function is zero. -/
theorem eq_zero_of_eventually {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {x : 𝕜} (hp : HasFPowerSeriesAt f p x)
    (hf : f =ᶠ[𝓝 x] 0) : p = 0 :=
  (hp.congr hf).eq_zero

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