prodMk — Mathlib

English

If HasStrictDerivAt f1 f1' x and HasStrictDerivAt f2 f2' x, then HasStrictDerivAt (λ t, (f1 t, f2 t)) (f1', f2') x.

Русский

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

LaTeX

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

Lean4

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

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