iterate — Mathlib

English

If f is differentiable within s at x, and f(x) = x, then all iterates f^[n] are differentiable within s at x.

Русский

Если f дифференцируема внутри s в x и x стабилен, то все итерации f^[n] дифференцируемы внутри s в x.

LaTeX

$$$$ \text{DifferentiableWithinAt } 𝕜 f s x \land f x = x \Rightarrow \forall n,\; \text{DifferentiableWithinAt } 𝕜 f^{[n]} s x. $$$$

Lean4

@[fun_prop]
protected theorem iterate {f : E → E} (hf : DifferentiableAt 𝕜 f x) (hx : f x = x) (n : ℕ) :
    DifferentiableAt 𝕜 f^[n] x :=
  (hf.hasFDerivAt.iterate hx n).differentiableAt

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