contMDiffOn_contMDiffCoordChange — Mathlib

English

There exists a contMDiffCoordChange for any pair of pretrivializations e and e' in the atlas; this change is affine-linear in the fiber variable.

Русский

Существование гладкого перехода координат.

LaTeX

$$$$\\exists (contMDiffCoordChange)\\; (n)\\,\\, e,e' \\,\\in a.pretrivializationAtlas.$$$$

Lean4

theorem contMDiffOn_contMDiffCoordChange (he : e ∈ a.pretrivializationAtlas) (he' : e' ∈ a.pretrivializationAtlas) :
    ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (a.contMDiffCoordChange n IB he he') (e.baseSet ∩ e'.baseSet) :=
  (Classical.choose_spec (ha.exists_contMDiffCoordChange e he e' he')).1

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