contMDiff — Mathlib

English

A smooth section induces a smooth map to the total space by pairing each base point with its value in the fiber.

Русский

Гладкая секция порождает гладкое отображение в обобщенном пространстве, соединяя базовую точку с её значением в волокне.

LaTeX

$$$\text{ContMDiffSection contMDiff: } s \mapsto (x \mapsto (x, s(x)))$ is smooth.$$

Lean4

protected theorem contMDiff (s : Cₛ^n⟮I; F, V⟯) :
    ContMDiff I (I.prod 𝓘(𝕜, F)) n fun x => TotalSpace.mk' F x (s x : V x) :=
  s.contMDiff_toFun

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