tangentBundle_model_space_coe_chartAt_symm

English

The inverse chartAt equals the product-space inverse chart; i.e., chartAt_symm coe equals toProd symm.

Русский

Обратная диаграмма chartAt совпадает с обратной диаграммой произведения пространства.

LaTeX

$$$((chartAt (ModelProd H E) p).symm) = (TotalSpace.toProd H E).symm$$$

Lean4

@[simp, mfld_simps]
theorem tangentBundle_model_space_coe_chartAt_symm (p : TangentBundle I H) :
    ((chartAt (ModelProd H E) p).symm : ModelProd H E → TangentBundle I H) = (TotalSpace.toProd H E).symm := by
  rw [← OpenPartialHomeomorph.coe_coe, OpenPartialHomeomorph.symm_toPartialEquiv, tangentBundle_model_space_chartAt];
  rfl

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