comp' — Mathlib

English

Same principle as above; composition preserves ContMDiffOn structure on domains.

Русский

Та же идея: композиция сохраняет ContMDiffOn на областях.

LaTeX

$$$hg: ContMDiffOn I' I'' n g t, \\\\ hf: ContMDiffOn I I' n f s, \\\\ st: s \\subseteq f^{-1}(t) \\\\Rightarrow ContMDiffOn I I'' n (g \\circ f) s$$$

Lean4

/-- The composition of `C^n` functions on domains is `C^n`. -/
theorem comp' {t : Set M'} {g : M' → M''} (hg : ContMDiffOn I' I'' n g t) (hf : ContMDiffOn I I' n f s) :
    ContMDiffOn I I'' n (g ∘ f) (s ∩ f ⁻¹' t) :=
  hg.comp (hf.mono inter_subset_left) inter_subset_right

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