contMDiffCoordChange_apply — Mathlib

English

The contMDiffOn property holds for the fiberwise linear coordination change map across any atlas entries of the VectorPrebundle.

Русский

Гладкость перехода координат по волокну.

LaTeX

$$$$\\text{ContMDiffOn }(a.contMDiffCoordChange) (e.baseSet \\cap e'.baseSet)$$$$

Lean4

theorem contMDiffCoordChange_apply (he : e ∈ a.pretrivializationAtlas) (he' : e' ∈ a.pretrivializationAtlas) {b : B}
    (hb : b ∈ e.baseSet ∩ e'.baseSet) (v : F) : a.contMDiffCoordChange n IB he he' b v = (e' ⟨b, e.symm b v⟩).2 :=
  (Classical.choose_spec (ha.exists_contMDiffCoordChange e he e' he')).2 b hb v

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