prodMk — Mathlib

English

If f and g are differentiable, then x ↦ (f x, g x) is differentiable with derivative df × dg.

Русский

Если f и g дифференцируемы, то x ↦ (f x, g x) дифференцируема с производной df × dg.

LaTeX

$$$ MDifferentiable I I' f \to MDifferentiable I I'' g \to MDifferentiable I (I' .prod I'') (fun x => (f x, g x)) $$$

Lean4

theorem prodMk {f : M → M'} {g : M → M''} (hf : MDifferentiable I I' f) (hg : MDifferentiable I I'' g) :
    MDifferentiable I (I'.prod I'') fun x => (f x, g x) := fun x => (hf x).prodMk (hg x)

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