continuousOn_fderivWithin_apply — Mathlib

English

A clarified version showing the differential operator applied to the second argument yields a ContDiffOn function on product domain.

Русский

Уточнённая версия: оператор дифференциирования применяется ко второму аргументу и даёт ContDiffOn на произведённой области.

LaTeX

$$$ContDiffOn\ 𝕜\ n\ f\ s \to\ ContDiffOn\ 𝕜\ m\ (\\lambda p. C\!ompose)\ (s\times univ)$$$

Lean4

/-- If a function is at least `C^1`, its bundled derivative (mapping `(x, v)` to `Df(x) v`) is
continuous. -/
theorem continuousOn_fderivWithin_apply (hf : ContDiffOn 𝕜 n f s) (hs : UniqueDiffOn 𝕜 s) (hn : 1 ≤ n) :
    ContinuousOn (fun p : E × E => (fderivWithin 𝕜 f s p.1 : E → F) p.2) (s ×ˢ univ) :=
  (contDiffOn_fderivWithin_apply (m := 0) hf hs hn).continuousOn

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