English
If hg : ContDiffWithinAt 𝕜 n g t y, hf : ContDiffWithinAt 𝕜 n f s x, and hy: f x = y, then ContDiffWithinAt 𝕜 n (g ∘ f) s x.
Русский
Если f x = y и g гладко на t в y, а f гладко на s в x, то g∘f гладко на s в x.
LaTeX
$$$ \operatorname{ContDiffWithinAt}_{\mathbb{K}}^{n} g\,t\,y \land \operatorname{ContDiffWithinAt}_{\mathbb{K}}^{n} f\,s\,x \land (f x = y) \Rightarrow \operatorname{ContDiffWithinAt}_{\mathbb{K}}^{n} (g \circ f)\,s\,x$$$
Lean4
/-- The composition of `C^n` functions at points in domains is `C^n`,
with a weaker condition on `s` and `t`. -/
theorem comp_of_mem_nhdsWithin_image {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) (hs : t ∈ 𝓝[f '' s] f x) :
ContDiffWithinAt 𝕜 n (g ∘ f) s x :=
(hg.mono_of_mem_nhdsWithin hs).comp x hf (subset_preimage_image f s)
