prodMk_space — Mathlib

English

If f is differentiable into E' and g into E'' on s, then their product into E' × E'' is differentiable on s.

Русский

Если f дифференцируемо в E', g — в E'' на s, то их произведение в E' × E'' дифференцируемо на s.

LaTeX

$$$ MDifferentiableOn I I' f s \to MDifferentiableOn I I'' g s \to MDifferentiableOn I (modelWithCornersSelf 𝕜 (Prod E' E'')) (fun x => { fst := f x, snd := g x }) s $$$

Lean4

theorem prodMk_space {f : M → E'} {g : M → E''} (hf : MDifferentiableOn I 𝓘(𝕜, E') f s)
    (hg : MDifferentiableOn I 𝓘(𝕜, E'') g s) : MDifferentiableOn I 𝓘(𝕜, E' × E'') (fun x => (f x, g x)) s := fun x hx =>
  (hf x hx).prodMk_space (hg x hx)

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