prodMk — Mathlib

English

If f1 and f2 are differentiable within a set s at x, then the map x ↦ (f1 x, f2 x) is differentiable within s at x.

Русский

Если функции f1 и f2 дифференцируемы внутри множества s в точке x, то отображение x ↦ (f1 x, f2 x) тоже дифференцируемо внутри s в x.

LaTeX

$$$\\text{DifferentiableWithinAt } 𝕜 f_1\; s\; x \\to \\text{ DifferentiableWithinAt } 𝕜 (\\lambda x:E, (f_1 x,f_2 x))\\; s\\; x$$

Lean4

@[fun_prop]
theorem prodMk (hf₁ : DifferentiableWithinAt 𝕜 f₁ s x) (hf₂ : DifferentiableWithinAt 𝕜 f₂ s x) :
    DifferentiableWithinAt 𝕜 (fun x : E => (f₁ x, f₂ x)) s x :=
  (hf₁.hasFDerivWithinAt.prodMk hf₂.hasFDerivWithinAt).differentiableWithinAt

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