prodMk — Mathlib

English

If f1 and f2 have derivatives f1' and f2' at x within s, then the map x ↦ (f1 x, f2 x) has derivative (f1', f2') within s at x.

Русский

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

LaTeX

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

Lean4

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

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