eq_formalMultilinearSeries_of_eventually

English

If hp and hq are HasFPowerSeriesAt for f and g respectively at x and f and g coincide eventually near x, then p = q.

Русский

Если hp и hq — представления FM для f и g в точке x и f совпадает с g в окрестности x почти повсеместно, то p = q.

LaTeX

$$$\\text{HasFPowerSeriesAt}\\, f\\, p\\, x\\rightarrow \\text{HasFPowerSeriesAt}\\, g\\, q\\, x \\rightarrow (f=_{\\text{nhds}(x)} g) \\Rightarrow p = q.$$$

Lean4

theorem eq_formalMultilinearSeries_of_eventually {p q : FormalMultilinearSeries 𝕜 𝕜 E} {f g : 𝕜 → E} {x : 𝕜}
    (hp : HasFPowerSeriesAt f p x) (hq : HasFPowerSeriesAt g q x) (heq : ∀ᶠ z in 𝓝 x, f z = g z) : p = q :=
  (hp.congr heq).eq_formalMultilinearSeries hq

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