comp_contDiff — Mathlib

English

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

Русский

Если g — C^n на s и f — C^n на всём, то g∘f — C^n на s.

LaTeX

$$$ \operatorname{ContDiffOn}_{\mathbb{K}}^{n} g\,s \Rightarrow \operatorname{ContDiff}_{\mathbb{K}}^{n} f \Rightarrow \operatorname{ContDiffOn}_{\mathbb{K}}^{n} (g\circ f)\,s$$$

Lean4

theorem comp_contDiff {s : Set F} {g : F → G} {f : E → F} (hg : ContDiffOn 𝕜 n g s) (hf : ContDiff 𝕜 n f)
    (hs : ∀ x, f x ∈ s) : ContDiff 𝕜 n (g ∘ f) :=
  by
  rw [← contDiffOn_univ] at *
  exact hg.comp hf fun x _ => hs x

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