contMDiff_proj — Mathlib

English

The projection map from the total space to the base space is C^n with respect to the chosen model of differentiability. In particular, the map π F E: TotalSpace F E → B is C^n.

Русский

Отображение проекции π F E: TotalSpace F E → B является C^n в рамках выбранной модели гладкости.

LaTeX

$$$\displaystyle \operatorname{ContMDiff} (IB. prod 𝓘(\mathit{𝕜}, F)) IB n \; \pi F E.$$$$

Lean4

theorem contMDiff_proj : ContMDiff (IB.prod 𝓘(𝕜, F)) IB n (π F E) := fun x ↦
  by
  have : ContMDiffAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n id x := contMDiffAt_id
  rw [contMDiffAt_totalSpace] at this
  exact this.1

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