comp_contMDiffOn — Mathlib

English

If g is C^n on all, and f is C^n on a set s, then g ∘ f is C^n on s.

Русский

Если g имеет класс C^n повсюду, а f — на множестве s, то g ∘ f имеет класс C^n на s.

LaTeX

$$$ ContMDiffOn I' I'' n g \;\to\; ContMDiffOn I I' n f s \;\Rightarrow\; ContMDiffOn I I'' n (g \circ f) s$$

Lean4

theorem comp_contMDiffOn {f : M → M'} {g : M' → M''} {s : Set M} (hg : ContMDiff I' I'' n g)
    (hf : ContMDiffOn I I' n f s) : ContMDiffOn I I'' n (g ∘ f) s :=
  hg.contMDiffOn.comp hf Set.subset_preimage_univ

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