prodMk — Mathlib

English

If f1 and f2 have strict Fréchet derivatives at a point, then the map x ↦ (f1 x, f2 x) has the product derivative given by the pair of derivatives.

Русский

Если у f1 и f2 есть строгие производные Фрéше, то x ↦ (f1 x, f2 x) имеет производную‑пару.

LaTeX

$$$\\text{HasStrictFDerivAt}(f_1,f_1',x) \\land \\text{HasStrictFDerivAt}(f_2,f_2',x) \\Rightarrow \\text{HasStrictFDerivAt}(x\\mapsto (f_1 x,f_2 x),(f_1',f_2'),x).$$$

Lean4

theorem prodMk (hf₁ : HasFDerivAtFilter f₁ f₁' x L) (hf₂ : HasFDerivAtFilter f₂ f₂' x L) :
    HasFDerivAtFilter (fun x => (f₁ x, f₂ x)) (f₁'.prod f₂') x L :=
  .of_isLittleO <| hf₁.isLittleO.prod_left hf₂.isLittleO

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