iteratedDerivWithin — Mathlib

English

Under uniqueness of the difference on s and differentiability at x, the iterated derivative within s equals the iterated derivative at x.

Русский

При условиях уникальности на s и дифференцируемости в x итеративная производная внутри s равна итеративной производной в точке x.

LaTeX

$$$ iteratedDerivWithin n f s x = iteratedDeriv n f x $$$

Lean4

/-- The `n`-th iterated derivative of a function from `𝕜` to `F` within a set `s`, as a function
from `𝕜` to `F`. -/
def iteratedDerivWithin (n : ℕ) (f : 𝕜 → F) (s : Set 𝕜) (x : 𝕜) : F :=
  (iteratedFDerivWithin 𝕜 n f s x : (Fin n → 𝕜) → F) fun _ : Fin n => 1

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