prodMk — Mathlib

English

If f,g are ContMDiffOn on s with model spaces, their product is ContMDiffOn into the product model.

Русский

Если f,g гладкие на s в пространстве модели, то их пара гладкая на s в произведении моделей.

LaTeX

$$ContMDiffOn I 𝓘(𝕜,E') n f s → ContMDiffOn I 𝓘(𝕜,F') n g s → ContMDiffOn I 𝓘(𝕜, E'×F') n (λ x, { fst := f x, snd := g x }) s$$

Lean4

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

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