contMDiffWithinAt_zeroSection — Mathlib

English

In a fixed base, the coordinate change map on fibers, given by a trivialization, is C^n along the base with respect to the base map f.

Русский

Координатное преобразование на волокнах, заданное тривиализацией, гладко по основанию относительно карты f.

LaTeX

$$$\displaystyle \operatorname{ContMDiffWithinAt} IB 𝓘(\mathit{𝕜}, F → L[𝕜] F) n (\\lambda y \\mapsto (e.coordChangeL 𝕜 e' (f y) : F →L[𝕜] F)) s x \\text{(условие)}$$$

Lean4

theorem contMDiffWithinAt_zeroSection {t : Set B} {x : B} :
    ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) n (zeroSection F E) t x :=
  (contMDiff_zeroSection _ _ x).contMDiffWithinAt

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