fderiv_succ — Mathlib

English

If f is C^{n+1} and g is C^n, then the map x ↦ fderiv 𝕜 (f x) (g x) is C^n.

Русский

Если f ∈ C^{n+1} и g ∈ C^n, то отображение x ↦ fderiv 𝕜 (f x) (g x) ∈ C^n.

LaTeX

$$$\operatorname{ContDiff}_{\mathbb{K}} n (\lambda x. fderiv 𝕜 (f x) (g x))$$$

Lean4

@[fun_prop]
protected theorem fderiv_succ {f : E → F → G} {g : E → F} (hf : ContDiffAt 𝕜 (m + 1) (Function.uncurry f) (x₀, g x₀))
    (hg : ContDiffAt 𝕜 m g x₀) : ContDiffAt 𝕜 m (fun x => fderiv 𝕜 (f x) (g x)) x₀ :=
  ContDiffAt.fderiv hf hg (le_refl _)

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