tangentBundleModelSpaceHomeomorph_coe

English

The homeomorphism tangentBundleModelSpaceHomeomorph between the tangent bundle and model space is the canonical product homeomorphism, i.e., it coincides with TotalSpace.toProd.

Русский

Гомеоморф между касательным расслоением и модельным пространством является каноническим произведением-гомеоморфом, совпадающим с TotalSpace.toProd.

LaTeX

$$$\mathrm{tangentBundleModelSpaceHomeomorph} : \TangentBundle I H \cong_t \mathrm{ModelProd} H E$ and its underlying map equals $\mathrm{TotalSpace.toProd}$$$

Lean4

@[simp, mfld_simps]
theorem tangentBundleModelSpaceHomeomorph_coe :
    (tangentBundleModelSpaceHomeomorph I : TangentBundle I H → ModelProd H E) = TotalSpace.toProd H E :=
  rfl

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