image_comp_contDiff — Mathlib

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)

Похожие утверждения