equivTangentBundleProd — Mathlib

English

Equivalences between tangent bundles respect product structure; canonical isomorphism between tangent bundles of product and product of tangent bundles.

Русский

Каноническое изоморфизм касательных пространств произведения и произведения касательных пространств.

LaTeX

$$$\mathrm{def}\ equivTangentBundleProd : TangentBundle (I .prod I') (M \times M') \simeq (TangentBundle I M) \times (TangentBundle I' M')$$$

Lean4

/-- The tangent bundle of a product is canonically isomorphic to the product of the tangent
bundles. -/
@[simps]
def equivTangentBundleProd : TangentBundle (I.prod I') (M × M') ≃ (TangentBundle I M) × (TangentBundle I' M')
    where
  toFun p := (⟨p.1.1, p.2.1⟩, ⟨p.1.2, p.2.2⟩)
  invFun p := ⟨(p.1.1, p.2.1), (p.1.2, p.2.2)⟩

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