hasFPowerSeriesWithinAt_insert — Mathlib

English

The zeroth coefficient of pf satisfies pf 0 v = f x for any v when hf holds.

Русский

Нулевой коэффициент pf удовлетворяет pf 0 v = f x для любого v, если hf выполняется.

LaTeX

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

Lean4

@[simp]
theorem hasFPowerSeriesWithinAt_insert {y : E} :
    HasFPowerSeriesWithinAt f p (insert y s) x ↔ HasFPowerSeriesWithinAt f p s x :=
  by
  rcases eq_or_ne x y with rfl | hy
  · simp [HasFPowerSeriesWithinAt]
  · refine ⟨fun h ↦ h.mono (subset_insert _ _), fun h ↦ ?_⟩
    apply HasFPowerSeriesWithinAt.mono_of_mem_nhdsWithin h
    rw [nhdsWithin_insert_of_ne hy]
    exact self_mem_nhdsWithin

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