comp_contMDiff — Mathlib

English

If g is ContMDiffOn on t and f is ContMDiff on s with f(s) ⊆ t, then g ∘ f is ContMDiffOn on s.

Русский

Если g C^n на t, а f C^n на s и f(s) ⊆ t, то g ∘ f C^n на s.

LaTeX

$$$\forall {f : M \to M'} {g : M' \to M''} {s : Set M} (hg : ContMDiffOn I' I'' n g t) (hf : ContMDiff I I' n f) (ht : ∀ x, f x \in t), ContMDiffOn I I'' n (g \circ f) s$$

Lean4

theorem comp_contMDiff {t : Set M'} {g : M' → M''} (hg : ContMDiffOn I' I'' n g t) (hf : ContMDiff I I' n f)
    (ht : ∀ x, f x ∈ t) : ContMDiff I I'' n (g ∘ f) :=
  contMDiffOn_univ.mp <| hg.comp hf.contMDiffOn fun x _ => ht x

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