prodMk — Mathlib

English

If f,g map into separate normed spaces E', E'', then (f,g) maps into their product E' × E'' with derivative df.prod dg.

Русский

Если f,g маппят в разные нормированные пространства E', E'', то (f,g) отображается в их произведение E' × E'' с производной df.prod dg.

LaTeX

$$$ MDifferentiableWithinAt I (I' prod I'') f s x \to MDifferentiableWithinAt I (I' prod I'') (fun x => (f x, g x)) s x $$$

Lean4

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

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