English
Let g be C^n differentiable on t at the point f(x), and f be C^n differentiable on s at x. Then the composition g ∘ f is C^n differentiable on the domain s ∩ f^{-1}(t) at x.
Русский
Пусть функция g имеет класс C^n на области t в точке f(x), а функция f имеет класс C^n на области s в точке x. Тогда композиция g ∘ f является C^n на области s ∩ f^{-1}(t) в точке x.
LaTeX
$$$\forall x\in E,\;\ContDiffWithinAt 𝕜 n\; g\; t\; (f x)\; \rightarrow\; \ContDiffWithinAt 𝕜 n\; f\; s\; x\; \rightarrow\; \ContDiffWithinAt 𝕜 n\; (g \circ f)\; (s \cap f^{-1}(t))\; x$$$
Lean4
/-- The composition of `C^n` functions at points in domains is `C^n`. -/
theorem comp_inter {s : Set E} {t : Set F} {g : F → G} {f : E → F} (x : E) (hg : ContDiffWithinAt 𝕜 n g t (f x))
(hf : ContDiffWithinAt 𝕜 n f s x) : ContDiffWithinAt 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t) x :=
hg.comp x (hf.mono inter_subset_left) inter_subset_right
