contMDiffAt_zeroSection

Mathlib.Geometry.Manifold.VectorBundle.Basic

URI: https://scilib.ai/kg/mathlib#Bundle.contMDiffAt_zeroSection

English

For any p in TotalSpace F E, the projection map π F E is C^n at p with respect to the product model.

Русский

Проекция π F E гладкая в точке p в рамках произведенной модели.

LaTeX

$$$\displaystyle \operatorname{contMDiffAt}_ {\text{prod}} (\pi F E)\; p\; n.$$$

Lean4

theorem contMDiffAt_zeroSection {x : B} : ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) n (zeroSection F E) x :=
  (contMDiff_zeroSection _ _).contMDiffAt

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru