English
The first iterated derivative within a set equals the one-dimensional derivative within that set: iteratedDerivWithin 1 f s x = derivWithin f s x.
Русский
Первая итеративная производная внутри множества равна однопеременной производной внутри множества: iteratedDerivWithin 1 f s x = derivWithin f s x.
LaTeX
$$$\operatorname{iteratedDerivWithin}\ 1\ f\ s\ x = \operatorname{derivWithin} f\ s\ x$$$
Lean4
@[simp]
theorem iteratedDerivWithin_one {x : 𝕜} : iteratedDerivWithin 1 f s x = derivWithin f s x :=
by
by_cases hsx : AccPt x (𝓟 s)
· simp only [iteratedDerivWithin, iteratedFDerivWithin_one_apply hsx.uniqueDiffWithinAt, derivWithin]
·
simp [derivWithin_zero_of_not_accPt hsx, iteratedDerivWithin, iteratedFDerivWithin,
fderivWithin_zero_of_not_accPt hsx]
