comp_differentiableOn — Mathlib

English

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

Русский

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

LaTeX

$$$$ \text{DifferentiableOn}_{\mathbb{K}} f s \to \text{MapsTo } f s s \to \forall n,\; \text{DifferentiableOn}_{\mathbb{K}} f^{[n]} s. $$$$

Lean4

@[fun_prop]
theorem comp_differentiableOn {g : F → G} (hg : Differentiable 𝕜 g) (hf : DifferentiableOn 𝕜 f s) :
    DifferentiableOn 𝕜 (g ∘ f) s :=
  hg.differentiableOn.comp hf (mapsTo_univ _ _)

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