eq_formalMultilinearSeries — Mathlib

English

Two formal multilinear series representing the same function at a point are equal.

Русский

Два формальных многолинейных ряда, представляющих одну и ту же функцию в точке, равны.

LaTeX

$$$\\text{HasFPowerSeriesAt}\\, f\\, p_1\\, x \\rightarrow \\text{HasFPowerSeriesAt}\\, f\\, p_2\\, x \\rightarrow p_1 = p_2.$$$

Lean4

/-- One-dimensional formal multilinear series representing the same function are equal. -/
theorem eq_formalMultilinearSeries {p₁ p₂ : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {x : 𝕜}
    (h₁ : HasFPowerSeriesAt f p₁ x) (h₂ : HasFPowerSeriesAt f p₂ x) : p₁ = p₂ :=
  sub_eq_zero.mp (HasFPowerSeriesAt.eq_zero (x := x) (by simpa only [sub_self] using h₁.sub h₂))

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