iterate — Mathlib

English

If f is differentiable within s at x, f(x) = x, and MapsTo f s s, then for every natural n, f^[n] is differentiable within s at x.

Русский

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

LaTeX

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

Lean4

@[fun_prop]
protected theorem iterate {f : E → E} (hf : DifferentiableWithinAt 𝕜 f s x) (hx : f x = x) (hs : MapsTo f s s) (n : ℕ) :
    DifferentiableWithinAt 𝕜 f^[n] s x :=
  (hf.hasFDerivWithinAt.iterate hx hs n).differentiableWithinAt

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