English
If g is C^n within t at f(x), f is C^n within s at x, and f^{-1}(t) belongs to the nhdsWithin filter at x restricted to s, then g ∘ f is C^n within s at x.
Русский
Если g имеет класс C^n внутри t в точке f(x), f имеет класс C^n внутри s в точке x, и предобраз t через f принадлежит nhdsWithin x в области s, то g ∘ f имеет класс C^n внутри s в x.
LaTeX
$$$\forall x\in E,\; \ContDiffWithinAt 𝕜 n\; g\; t\; (f x)\; \rightarrow\; \ContDiffWithinAt 𝕜 n\; f\; s\; x\; \rightarrow\ f^{-1}(t) \in 𝓝[s] x \rightarrow \ContDiffWithinAt 𝕜 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_preimage_mem_nhdsWithin {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 : f ⁻¹' t ∈ 𝓝[s] x) :
ContDiffWithinAt 𝕜 n (g ∘ f) s x :=
(hg.comp_inter x hf).mono_of_mem_nhdsWithin (inter_mem self_mem_nhdsWithin hs)
