comp — Mathlib

English

The composition of two C^n maps is again a C^n map.

Русский

Композиция двух C^n отображений снова является C^n отображением.

LaTeX

$$$\text{comp}(f,g) : C^n⟮I, M; I', M'⟯ \to C^n⟮I, M; I'', M''⟯$, defined by $(f,g) \mapsto a \mapsto f(g(a))$ with the smoothness proof $f.contMDiff.comp g.contMDiff$$$

Lean4

/-- The composition of `C^n` maps, as a `C^n` map. -/
def comp (f : C^n⟮I', M'; I'', M''⟯) (g : C^n⟮I, M; I', M'⟯) : C^n⟮I, M; I'', M''⟯
    where
  val a := f (g a)
  property := f.contMDiff.comp g.contMDiff

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