iteratedFDerivWithin_one_apply — Mathlib

English

For a set s with UniqueDiffOn, the order-1 iterated derivative applied to a 1-element m reduces to applying fderivWithin at x to m0.

Русский

Для множества s с UniqueDiffOn применение первой итерационной производной к однобитному аргументу m сводится к применению fderivWithin в точке x к m0.

LaTeX

$$$\big( \operatorname{iteratedFDerivWithin}_{\mathbb{K}}^{(1)} f\, s\, x \big)\, m = fderivWithin_{\mathbb{K}} f\, s\, x\, (m_0)$$$

Lean4

@[simp]
theorem iteratedFDerivWithin_one_apply (h : UniqueDiffWithinAt 𝕜 s x) (m : Fin 1 → E) :
    iteratedFDerivWithin 𝕜 1 f s x m = fderivWithin 𝕜 f s x (m 0) := by
  simp [iteratedFDerivWithin_succ_apply_left, iteratedFDerivWithin_zero_eq_comp,
    (continuousMultilinearCurryFin0 𝕜 E F).symm.comp_fderivWithin h]

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