contMDiffOn_zeroSection — Mathlib

English

Within a subset s of TotalSpace F E, the projection π F E remains C^n at p; i.e., the projection is differentiable with the same regularity on that set.

Русский

Внутри подмножества s всего пространства проекция остаётся C^n в точке p.

LaTeX

$$$\displaystyle \operatorname{ContMDiffWithinAt} (IB. prod 𝓘(𝕜, F)) IB n \; \pi F E \ s\ p := \dots$$$

Lean4

theorem contMDiffOn_zeroSection {t : Set B} : ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) n (zeroSection F E) t :=
  (contMDiff_zeroSection _ _).contMDiffOn

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