comp — Mathlib

English

Let f: M → M' and g: M' → M'' be ContMDiffAt n at the relevant points. Then the composition g ∘ f is ContMDiffAt n at x.

Русский

Пусть f: M → M' и g: M' → M'' имеют класс ContMDiffAt n в соответствующих точках. Тогда композиция g ∘ f имеет класс ContMDiffAt n в точке x.

LaTeX

$$$\forall {x : M},\; ContMDiffAt I' I'' n g (f x) \;\land\; ContMDiffAt I I' n f x \Rightarrow ContMDiffAt I I'' n (g \circ f) x$$

Lean4

/-- The composition of `C^n` functions at points is `C^n`. -/
nonrec theorem comp {g : M' → M''} (x : M) (hg : ContMDiffAt I' I'' n g (f x)) (hf : ContMDiffAt I I' n f x) :
    ContMDiffAt I I'' n (g ∘ f) x :=
  hg.comp x hf (mapsTo_univ _ _)

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