tangentMap_prodSnd — Mathlib

English

The tangent map of the product projection to the second component is given by sending a tangent vector to the second component with the appropriate basepoint shift.

Русский

Касательная карта проекции на вторую компоненту переводит вектор касательных к второй компоненте, учитывая базовую точку.

LaTeX

$$$\text{tangentMap } (I.{\prod} I')\ I' Prod.snd\ p = ⟨p.proj.2, p.2.2⟩$$$

Lean4

@[simp, mfld_simps]
theorem tangentMap_prodSnd {p : TangentBundle (I.prod I') (M × M')} :
    tangentMap (I.prod I') I' Prod.snd p = ⟨p.proj.2, p.2.2⟩ := by simp [tangentMap]; rfl

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