tangentBundleCore_coordChange_model_space

English

In model space, the coordinate change between any two coordinates is the identity map; i.e., coordChange = id.

Русский

В модельном пространстве координатное изменение между любыми двумя координатами равно тождественному отображению.

LaTeX

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

Lean4

theorem tangentBundleCore_coordChange_model_space (x x' z : H) :
    (tangentBundleCore I H).coordChange (achart H x) (achart H x') z = ContinuousLinearMap.id 𝕜 E := by ext v;
  exact (tangentBundleCore I H).coordChange_self (achart _ z) z (mem_univ _) v

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