prodMk — Mathlib

English

If f1 and f2 have differentiable-at derivatives at x, then the map x ↦ (f1 x, f2 x) has the differential equal to the pair of differentials.

Русский

Если у f1 и f2 есть производная, то x ↦ (f1 x, f2 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₁ : HasFDerivWithinAt f₁ f₁' s x) (hf₂ : HasFDerivWithinAt f₂ f₂' s x) :
    HasFDerivWithinAt (fun x => (f₁ x, f₂ x)) (f₁'.prod f₂') s x :=
  hf₁.prodMk hf₂

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