comp — Mathlib

English

The composition of C^n maps on domains is C^n on the domain, provided the image stays within the domain of the outer map.

Русский

Сложение C^n отображений на областях есть C^n на области, если образ f области лежит внутри области определения g.

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)
    (st : s ⊆ f ⁻¹' t) : ContMDiffOn I I'' n (g ∘ f) s := fun x hx => (hg _ (st hx)).comp x (hf x hx) st

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