contDiff_fderiv_apply — Mathlib

English

If f is C^n, then the map x ↦ fderiv 𝕜 (f x) (g x) (k x) is C^n, given m+1 ≤ n.

Русский

Если f имеет гладкость C^n, то отображение x ↦ fderiv 𝕜 (f x) (g x) (k x) является C^n при условии m+1 ≤ n.

LaTeX

$$$ContDiff\ 𝕜\ n\ (Function.uncurry\ f) \to ContDiff\ 𝕜\ m\ (\lambda x. fderiv 𝕜 (f x) (g x) (k x))$$$

Lean4

/-- The bundled derivative of a `C^{n+1}` function is `C^n`. -/
theorem contDiff_fderiv_apply {f : E → F} (hf : ContDiff 𝕜 n f) (hmn : m + 1 ≤ n) :
    ContDiff 𝕜 m fun p : E × E => (fderiv 𝕜 f p.1 : E →L[𝕜] F) p.2 :=
  by
  rw [← contDiffOn_univ] at hf ⊢
  rw [← fderivWithin_univ, ← univ_prod_univ]
  exact contDiffOn_fderivWithin_apply hf uniqueDiffOn_univ hmn

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