iteratedDerivWithin_succ' — Mathlib

English

Similar reformulation: iteratedDerivWithin n f s x equals the nth iterate of the derivWithin operator applied to f at x.

Русский

Аналогично: iteratedDerivWithin n f s x равна n-му повторному применению оператора derivWithin к f в точке x.

LaTeX

$$$\operatorname{iteratedDerivWithin} n f s x = (\text{function applying } \operatorname{derivWithin} s)^{[n]} f (x)$$$

Lean4

/-- The `n+1`-th iterated derivative within a set with unique derivatives can be obtained by
taking the `n`-th derivative of the derivative. -/
theorem iteratedDerivWithin_succ' {x : 𝕜} :
    iteratedDerivWithin (n + 1) f s x = (iteratedDerivWithin n (derivWithin f s) s) x := by
  rw [iteratedDerivWithin_eq_iterate, iteratedDerivWithin_eq_iterate]; rfl

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