prodMk — Mathlib

English

If HasDerivAt f1 f1' x and HasDerivAt f2 f2' x, then the pairing map x ↦ (f1 x, f2 x) has derivative (f1', f2') at x.

Русский

Если у функций f1 и f2 есть производные f1' и f2' в точке x по HasDerivAt, то отображение x ↦ (f1 x, f2 x) имеет производную (f1', f2') в x.

LaTeX

$$$HasDerivAt f_1 f_1' x \to HasDerivAt f_2 f_2' x \to HasDerivAt (\lambda t, (f_1 t, f_2 t)) (f_1', f_2') x$$$

Lean4

nonrec theorem prodMk (hf₁ : HasDerivAt f₁ f₁' x) (hf₂ : HasDerivAt f₂ f₂' x) :
    HasDerivAt (fun x => (f₁ x, f₂ x)) (f₁', f₂') x :=
  hf₁.prodMk hf₂

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