prodMk — Mathlib

English

Repeated product-derivative rule for pairs under HasFDerivAt with respect to x.

Русский

Повторно применимо правило производной пары по x.

LaTeX

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

Lean4

@[fun_prop]
nonrec theorem prodMk (hf₁ : HasFDerivAt f₁ f₁' x) (hf₂ : HasFDerivAt f₂ f₂' x) :
    HasFDerivAt (fun x => (f₁ x, f₂ x)) (f₁'.prod f₂') x :=
  hf₁.prodMk hf₂

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