clm_comp — Mathlib

English

Same as above: differentiability is preserved along all iterates of f at x when f is differentiable at x and f(x) = x.

Русский

То же самое: сохраняется дифференцируемость по всем итерациям f^[n] в x, если f дифференцируема в x и f(x)=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 : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) :
    DifferentiableAt 𝕜 (fun y => (c y).comp (d y)) x :=
  (hc.hasFDerivAt.clm_comp hd.hasFDerivAt).differentiableAt

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