contMDiffCoordChange — Mathlib

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

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