prodMk — Mathlib

English

If f and g are differentiable on a set s, then the map x ↦ (f x, g x) is differentiable on s with derivative df × dg.

Русский

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

LaTeX

$$$ prodMk {f : M \to M'} {g : M \to M''} (hf : MDifferentiableOn I I' f s) (hg : MDifferentiableOn I I'' g s) : MDifferentiableOn I (I'.prod I'') (fun x => (f x, g x)) s $$$

Lean4

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

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