comp_of_mem_nhdsWithin_image_of_eq

English

If hg : ContDiffOn 𝕜 n g (f '' s) and hf : ContDiff 𝕜 n f, then ContDiffOn 𝕜 n (g ∘ f) s.

Русский

Если g гладкая на изображении f(s) и f сама гладкая, то композиция гладкая на 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

/-- 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_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) (hs : t ∈ 𝓝[f '' s] f x) (hy : f x = y) :
    ContDiffWithinAt 𝕜 n (g ∘ f) s x := by subst hy; exact hg.comp_of_mem_nhdsWithin_image x hf hs

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