English
If hg : ContDiffOn 𝕜 n g (f '' s) and hf : ContDiff 𝕜 n f, then ContDiffOn 𝕜 n (g ∘ f) s.
Русский
Если g — ContDiffOn на изображении f(s) и f — ContDiff, тогда g∘f — ContDiffOn на s.
LaTeX
$$$ \operatorname{ContDiffOn}_{\mathbb{K}}^{n} g \,(f''s) \land \operatorname{ContDiff}_{\mathbb{K}}^{n} f \Rightarrow \operatorname{ContDiffOn}_{\mathbb{K}}^{n} (g\circ f)\,s $$$
Lean4
theorem image_comp_contDiff {s : Set E} {g : F → G} {f : E → F} (hg : ContDiffOn 𝕜 n g (f '' s)) (hf : ContDiff 𝕜 n f) :
ContDiffOn 𝕜 n (g ∘ f) s :=
hg.comp hf.contDiffOn (s.mapsTo_image f)