English
The contMDiffOn property for a VectorPrebundle ensures the contMDiffCoordChange map is C^n on the intersection of atlas trivilizations.
Русский
Переход координат гладок.
LaTeX
$$$$\\text{ContMDiffOn }(a.contMDiffCoordChange) (e.baseSet \\cap e'.baseSet)$$$$
Lean4
/-- A randomly chosen coordinate change on a `VectorPrebundle` satisfying `IsContMDiff`, given by
the field `exists_coordChange`. Note that `a.contMDiffCoordChange` need not be the same as
`a.coordChange`. -/
noncomputable def contMDiffCoordChange (he : e ∈ a.pretrivializationAtlas) (he' : e' ∈ a.pretrivializationAtlas)
(b : B) : F →L[𝕜] F :=
Classical.choose (ha.exists_contMDiffCoordChange e he e' he') b