fderiv_succ — Mathlib

English

If f is C^n and g is C^n, then the map x ↦ fderiv 𝕜 f x (g x) is ContDiff.

Русский

Если f и g гладкие, то отображение x ↦ fderiv 𝕜 f x (g x) гладко.

LaTeX

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

Lean4

@[fun_prop]
protected theorem fderiv_succ {f : E → F → G} {g : E → F} (hf : ContDiff 𝕜 (n + 1) <| Function.uncurry f)
    (hg : ContDiff 𝕜 n g) : ContDiff 𝕜 n fun x => fderiv 𝕜 (f x) (g x) :=
  contDiff_iff_contDiffAt.mpr fun _ => hf.contDiffAt.fderiv hg.contDiffAt (le_refl (n + 1))

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