prodMk — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp, fun_prop]
theorem prodMk (hf₁ : DifferentiableAt 𝕜 f₁ x) (hf₂ : DifferentiableAt 𝕜 f₂ x) :
    DifferentiableAt 𝕜 (fun x : E => (f₁ x, f₂ x)) x :=
  (hf₁.hasFDerivAt.prodMk hf₂.hasFDerivAt).differentiableAt

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