prodMk — Mathlib

English

If f1 and f2 have differentiable-at derivatives along a filter, then the map x ↦ (f1 x, f2 x) has derivative given by the product of derivatives.

Русский

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

LaTeX

$$$\\text{HasFDerivAtFilter}(f_1,f_1',x,L) \\land \\text{HasFDerivAtFilter}(f_2,f_2',x,L) \\\\rightarrow \\text{HasFDerivAtFilter}(x\\mapsto (f_1 x,f_2 x),(f_1',f_2'),x,L).$$$

Lean4

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

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