comp_of_eq — Mathlib

English

If f: 𝕜 → 𝕜 is differentiable at x with strict derivative f′ and x is a fixed point (f x = x), then the nth iterate f^[n] has derivative f′^n at x.

Русский

Если f: 𝕜 → 𝕜 дифференцируема в x с строгой производной f′ и x является фиксированной точкой (f x = x), то n-й перебор f^[n] имеет производную f′^n в x.

LaTeX

$$$$\\forall x:\\; \\text{HasStrictDerivAt}(f,f',x) \\land f(x)=x \\Rightarrow \\text{HasStrictDerivAt}(f^{[n]},(f')^{n},x). $$$$

Lean4

theorem comp_of_eq (hh₂ : HasDerivWithinAt h₂ h₂' s' y) (hh : HasDerivWithinAt h h' s x) (hst : MapsTo h s s')
    (hy : y = h x) : HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x := by rw [hy] at hh₂; exact hh₂.comp x hh hst

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