prodMk — Mathlib

English

If f and g are ContMDiffAt at a point x, then the map x ↦ (f x, g x) is ContMDiffAt at x with the product model.

Русский

Если f и g гладкие в точке x, то x ↦ (f(x), g(x)) гладко в точке x в произведении моделей.

LaTeX

$$ContMDiffAt I I' n f x → ContMDiffAt I J' n g x → ContMDiffAt I (I'.prod J') n (λ x, (f x, g x)) x$$

Lean4

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

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