fderiv — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- `x ↦ fderiv 𝕜 (f x) (g x)` is smooth. -/
protected theorem fderiv {f : E → F → G} {g : E → F} (hf : ContDiff 𝕜 m <| Function.uncurry f) (hg : ContDiff 𝕜 n g)
    (hnm : n + 1 ≤ m) : ContDiff 𝕜 n fun x => fderiv 𝕜 (f x) (g x) :=
  contDiff_iff_contDiffAt.mpr fun _ => hf.contDiffAt.fderiv hg.contDiffAt hnm

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