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