English
If hf : ContDiffOn 𝕜 n f s and hg : ContDiffOn 𝕜 n g s, then ContDiffOn 𝕜 n (y ↦ (f y, g y)) s.
Русский
Если hf : ContDiffOn 𝕜 n f s и hg : ContDiffOn 𝕜 n g s, то ContDiffOn 𝕜 n (y ↦ (f y, g y)) s.
LaTeX
$$$ \operatorname{ContDiffOn}_{\mathbb{K}}^{n} f\,s \;\land\; \operatorname{ContDiffOn}_{\mathbb{K}}^{n} g\,s\ \Rightarrow\ \operatorname{ContDiffOn}_{\mathbb{K}}^{n} (\;y \mapsto (f(y),g(y))\;)\,s$$$
Lean4
/-- The Cartesian product of `C^n` functions at a point in a domain is `C^n`. -/
@[fun_prop]
theorem prodMk {s : Set E} {f : E → F} {g : E → G} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) :
ContDiffWithinAt 𝕜 n (fun x : E => (f x, g x)) s x := by
match n with
| ω =>
obtain ⟨u, hu, p, hp, h'p⟩ := hf
obtain ⟨v, hv, q, hq, h'q⟩ := hg
refine
⟨u ∩ v, Filter.inter_mem hu hv, _, (hp.mono inter_subset_left).prodMk (hq.mono inter_subset_right), fun i ↦ ?_⟩
change AnalyticOn 𝕜 (fun x ↦ ContinuousMultilinearMap.prodL _ _ _ _ (p x i, q x i)) (u ∩ v)
apply (LinearIsometryEquiv.analyticOnNhd _ _).comp_analyticOn _ (Set.mapsTo_univ _ _)
exact ((h'p i).mono inter_subset_left).prod ((h'q i).mono inter_subset_right)
| (n : ℕ∞) =>
intro m hm
rcases hf m hm with ⟨u, hu, p, hp⟩
rcases hg m hm with ⟨v, hv, q, hq⟩
exact ⟨u ∩ v, Filter.inter_mem hu hv, _, (hp.mono inter_subset_left).prodMk (hq.mono inter_subset_right)⟩
