comp — Mathlib

English

If f is differentiable, then all iterates f^[n] are differentiable for every n.

Русский

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

LaTeX

$$$$ \\text{Differentiable}_{\\mathbb{K}} f \\;\to\ \forall n \\in \\mathbb{N},\; \\text{Differentiable}_{\\mathbb{K}} (f^{[n]}). $$$$

Lean4

@[fun_prop]
theorem comp {g : F → G} (hg : Differentiable 𝕜 g) (hf : Differentiable 𝕜 f) : Differentiable 𝕜 (g ∘ f) := fun x =>
  DifferentiableAt.comp x (hg (f x)) (hf x)

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