English
Let y ∈ F be such that g is C^n at y on t, and f is C^n within s at x with f(x) = y. Then the composition g ∘ f is C^n within s at x.
Русский
Пусть y ∈ F так, что g имеет класс C^n в точке y на t, и f имеет класс C^n внутри s в точке x при условии f(x) = y. Тогда композиция g ∘ f имеет класс C^n внутри s в x.
LaTeX
$$$\forall x\in E,\; \ContDiffWithinAt 𝕜 n\; g\; t\; y\; \rightarrow\; \ContDiffWithinAt 𝕜 n\; f\; s\; x\; \rightarrow\; f x = y \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_of_eq {s : Set E} {t : Set F} {g : F → G} {f : E → F} {y : F} (x : E)
(hg : ContDiffWithinAt 𝕜 n g t y) (hf : ContDiffWithinAt 𝕜 n f s x) (hy : f x = y) :
ContDiffWithinAt 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t) x := by subst hy; exact hg.comp_inter x hf
