coordChange_model_space — Mathlib

English

In model space, the coordinate change along any x, x' in H is the identity map; i.e., coordChange on the model space equals 1.

Русский

В модельном пространстве координатное изменение между чартаками x и x' является тождественным отображением; то есть coordChange = 1.

LaTeX

$$$(\mathrm{tangentBundleCore}\; (\mathrm{modelWithCornersSelf}\ 𝕜\ F)\; F).coordChange (\operatorname{achart} F b) (\operatorname{achart} F b') x = 1$$$

Lean4

@[simp high, mfld_simps]
theorem coordChange_model_space (b b' x : F) :
    (tangentBundleCore 𝓘(𝕜, F) F).coordChange (achart F b) (achart F b') x = 1 := by
  simpa only [tangentBundleCore_coordChange, mfld_simps] using fderivWithin_id uniqueDiffWithinAt_univ

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