contMDiffAt_proj — Mathlib

English

The zero section is C^n on any subset t of the base space: the restriction of the zero section to t is a C^n map.

Русский

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

LaTeX

$$$\displaystyle \operatorname{ContMDiffOn} IB (IB. prod 𝓘(𝕜, F)) n (\text{zeroSection } F E) t.$$$

Lean4

theorem contMDiffAt_proj {p : TotalSpace F E} : ContMDiffAt (IB.prod 𝓘(𝕜, F)) IB n (π F E) p :=
  (contMDiff_proj E).contMDiffAt

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