prodMk_space — Mathlib

English

If f and g are C^n at a point, then the product map x ↦ (f x, g x) is C^n at that point into the product space.

Русский

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

LaTeX

$$ContMDiffAt I 𝓘(𝕜, E') n f x → ContMDiffAt I 𝓘(𝕜, F') n g x → ContMDiffAt I 𝓘(𝕜, E'×F') n (λ x, (f x, g x)) x$$

Lean4

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

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