ftaylorSeriesWithin_insert — Mathlib

English

The insert shortcut extends to the standard iterated derivative insert identities.

Русский

Расширение вставки применяется к обычному правилу вставки для производной н-ого порядка.

LaTeX

$$$\forall n, iteratedFDerivWithin 𝕜 n f (insert x s) y = iteratedFDerivWithin 𝕜 n f s y$$$

Lean4

@[simp]
theorem ftaylorSeriesWithin_insert : ftaylorSeriesWithin 𝕜 f (insert x s) = ftaylorSeriesWithin 𝕜 f s :=
  by
  ext y n : 2
  apply iteratedFDerivWithin_insert

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