fderiv_one — Mathlib

English

If f is C^1 in the uncurry sense and g is continuous, then the map x ↦ fderiv 𝕜 (f x) (g x) is continuous.

Русский

Если f имеет класс C^1 в виде uncurry и g непрерывна, то отображение x ↦ fderiv 𝕜 (f x) (g x) непрерывно.

LaTeX

$$$ContDiff\ 𝕜\ 1\ (Function.uncurry\ f)\; \to\; Continuous\ g\;\to\; Continuous\left( x \mapsto fderiv\ 𝕜\ (f x)\ (g x)\right)$$$

Lean4

@[fun_prop]
theorem fderiv_one {f : E → F → G} {g : E → F} (hf : ContDiff 𝕜 1 <| Function.uncurry f) (hg : Continuous g) :
    Continuous fun x => _root_.fderiv 𝕜 (f x) (g x) :=
  (hf.fderiv (contDiff_zero.mpr hg) (le_refl 1)).continuous

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