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