prodMk — Mathlib

English

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

Русский

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

LaTeX

$$$ prodMk {f : M → M'} {g : M → M''} (hf : MDifferentiableWithinAt I I' f s x) (hg : MDifferentiableWithinAt I I'' g s x) : MDifferentiableWithinAt I (I'.prod I'') (fun y => (f y, g y)) s x (df.prod dg) $$$

Lean4

theorem prodMk {f : M → M'} {g : M → M''} (hf : MDifferentiableWithinAt I I' f s x)
    (hg : MDifferentiableWithinAt I I'' g s x) : MDifferentiableWithinAt I (I'.prod I'') (fun x => (f x, g x)) s x :=
  ⟨hf.1.prodMk hg.1, hf.2.prodMk hg.2⟩

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