hasFPowerSeriesWithinOnBall_insert_self

English

The zeroth coefficient of the formal power series equals the value at the base point.

Русский

Нулевой коэффициент формальной степенной серии равен значению функции в базовой точке.

LaTeX

$$$HasFPowerSeriesWithinOnBall f pf s x r \\Rightarrow pf 0 v = f x$ for any v : Fin 0 → E.$$

Lean4

@[simp]
theorem hasFPowerSeriesWithinOnBall_insert_self :
    HasFPowerSeriesWithinOnBall f p (insert x s) x r ↔ HasFPowerSeriesWithinOnBall f p s x r := by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ <;>
    exact ⟨h.r_le, h.r_pos, fun {y} ↦ by simpa only [insert_idem] using h.hasSum (y := y)⟩

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