ContMDiffWithinAt.prod_mk_space

theorem ContMDiffWithinAt.prod_mk_space : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace 𝕜 E'] {F' : Type u_14} [inst_8 : NormedAddCommGroup F'] [inst_9 : NormedSpace 𝕜 F'] {s : Set M} {x : M} {n : ℕ∞} {f : M → E'} {g : M → F'}, ContMDiffWithinAt I (modelWithCornersSelf 𝕜 E') n f s x → ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F') n g s x → ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (E' × F')) n (fun x => (f x, g x)) s x

This theorem, `ContMDiffWithinAt.prod_mk_space`, states that for a given non-trivially normed field `𝕜`, types `E`, `H`, `M`, `E'`, `F'` equipped with required structures, a set `s` of type `M`, an element `x` of type `M`, and `n` of type `ℕ∞` (which can be a natural number or infinity), if the functions `f : M → E'` and `g : M → F'` are continuously differentiable within the set `s` at the point `x` under the model with corners `I` and the respective model spaces `E'` and `F'`, then the function that maps `x` to the pair `(f x, g x)` in the product space `E' × F'` is also continuously differentiable at `x` within `s` under the model with corners `I` and the product model space `E' × F'`.

More concisely: If functions `f` and `g` are continuously differentiable at a point `x` in set `s` of type `M` with respect to non-trivially normed field `𝕜`, then the function mapping `x` to `(f x, g x)` in `E' × F'` is also continuously differentiable at `x` within `s`.