contDiffOn_fderivWithin_apply — Mathlib

English

Symmetric variant: the same C^n-closure of the bundled derivative under additional structure.

Русский

Симметричный вариант: такая же гладкость как и выше для связанной производной внутри области.

LaTeX

$$$ContDiffOn\ 𝕜\ n\ f\ s\; \to\; ContDiffOn\ 𝕜\ n\ (\\lambda p. fderivWithin\ 𝕜\ f\ s\ p.1)\ p.snd$$$

Lean4

/-- The bundled derivative of a `C^{n+1}` function is `C^n`. -/
theorem contDiffOn_fderivWithin_apply {s : Set E} {f : E → F} (hf : ContDiffOn 𝕜 n f s) (hs : UniqueDiffOn 𝕜 s)
    (hmn : m + 1 ≤ n) : ContDiffOn 𝕜 m (fun p : E × E => (fderivWithin 𝕜 f s p.1 : E →L[𝕜] F) p.2) (s ×ˢ univ) :=
  ((hf.fderivWithin hs hmn).comp contDiffOn_fst (prod_subset_preimage_fst _ _)).clm_apply contDiffOn_snd

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