English
If f has a derivative within s at x, f(x) = x, and MapsTo f s s, then for every n, HasFDerivWithinAt f^[n] at x with derivative (f')^n.
Русский
Если у f есть производная внутри s в x и f(x) = x, и MapsTo f s s, тогда для каждого n существует HasFDerivWithinAt для f^[n] в x с производной (f')^n.
LaTeX
$$$$ \text{HasFDerivWithinAt } f f' s x \land f(x) = x \land \text{MapsTo } f s s \Rightarrow \forall n,\; \text{HasFDerivWithinAt } f^{[n]} (f')^{n} s x. $$$$
Lean4
@[fun_prop]
protected theorem iterate {f : E → E} {f' : E →L[𝕜] E} (hf : HasFDerivAt f f' x) (hx : f x = x) (n : ℕ) :
HasFDerivAt f^[n] (f' ^ n) x := by
refine HasFDerivAtFilter.iterate hf ?_ hx n
convert hf.continuousAt.tendsto
exact hx.symm
