contMDiffOn_proj — Mathlib

English

The zero section of a vector bundle, which assigns to each base point the zero vector in the corresponding fiber, is C^n as a map from the base to the total space.

Русский

Нулевая секция векторного расслоения является C^n как отображение базы в общее пространство.

LaTeX

$$$\displaystyle \operatorname{ContMDiffAt}\; IB\; (IB. prod\; 𝓘(𝕜, F))\; n\; (\text{zeroSection } F E)\ x.$$$

Lean4

theorem contMDiffOn_proj {s : Set (TotalSpace F E)} : ContMDiffOn (IB.prod 𝓘(𝕜, F)) IB n (π F E) s :=
  (contMDiff_proj E).contMDiffOn

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