comp_contMDiffWithinAt — Mathlib

English

Basic chain rule for ContMDiff in the presence of charts and model-with-corners.

Русский

Основное правило цепи для ContMDiff с учётом диаграмм и модели углов.

LaTeX

$$$ContMDiffWithinAt.comp' \\\\text{(quoted)}$$$

Lean4

/-- `g ∘ f` is `C^n` within `s` at `x` if `g` is `C^n` at `f x` and
`f` is `C^n` within `s` at `x`. -/
theorem comp_contMDiffWithinAt {g : M' → M''} (x : M) (hg : ContMDiffAt I' I'' n g (f x))
    (hf : ContMDiffWithinAt I I' n f s x) : ContMDiffWithinAt I I'' n (g ∘ f) s x :=
  hg.comp x hf (mapsTo_univ _ _)

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