comp — Mathlib

English

If hg : ContDiff 𝕜 n g and hf : ContDiffOn 𝕜 n f s, then ContDiffOn 𝕜 n (fun x => g (f x)) s.

Русский

Если g — C^n, а f — C^n на s, тогда x ↦ g(f(x)) — ContDiffOn 𝕜 n на s.

LaTeX

$$$ \operatorname{ContDiff}_{\mathbb{K}}^{n} g \Rightarrow \operatorname{ContDiffOn}_{\mathbb{K}}^{n} f \Rightarrow \operatorname{ContDiffOn}_{\mathbb{K}}^{n} (x \mapsto g (f x))$$$

Lean4

/-- The composition of `C^n` functions is `C^n`. -/
theorem comp {g : F → G} {f : E → F} (hg : ContDiff 𝕜 n g) (hf : ContDiff 𝕜 n f) : ContDiff 𝕜 n (g ∘ f) :=
  contDiffOn_univ.1 <| ContDiffOn.comp (contDiffOn_univ.2 hg) (contDiffOn_univ.2 hf) (subset_univ _)

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