clm_comp — Mathlib

English

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

Русский

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

LaTeX

$$$$ \text{DifferentiableAt } 𝕜 f x \land f x = x \Rightarrow \forall n, \; \text{DifferentiableAt } 𝕜 (Nat.iterate f n) x. $$$$

Lean4

@[fun_prop]
theorem clm_comp (hc : DifferentiableWithinAt 𝕜 c s x) (hd : DifferentiableWithinAt 𝕜 d s x) :
    DifferentiableWithinAt 𝕜 (fun y => (c y).comp (d y)) s x :=
  (hc.hasFDerivWithinAt.clm_comp hd.hasFDerivWithinAt).differentiableWithinAt

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