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