prodMk — Mathlib

English

Within a set s, the derivative of the product map equals the product of derivatives: fderivWithin 𝕜 (λ x, (f1 x, f2 x)) s x = (fderivWithin 𝕜 f1 s x) .prod (fderivWithin 𝕜 f2 s x), assuming UniqueDiffWithinAt 𝕜 s x.

Русский

Внутри множества s производная от отображения x ↦ (f1 x, f2 x) равна произведению производных, при условии UniqueDiffWithinAt 𝕜 s x.

LaTeX

$$$\text{fderivWithin } 𝕜 (\lambda x:E, (f_1 x,f_2 x)) s x = (\text{fderivWithin } 𝕜 f_1 s x) .prod (\text{fderivWithin } 𝕜 f_2 s x)$$$

Lean4

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

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