mfderiv_fst — Mathlib

English

Let p be a tangent vector in the product tangent bundle. The tangent map of fst at p sends p to (proj.1, p.2.1), i.e. the output lives in the tangent space of M together with the first component of the second factor.

Русский

Пусть p — касательное вектор в касательном произведении. Производная касательного отображения fst в p отправляет p в (proj.1, p.2.1).

LaTeX

$$$\mathrm{tangentMap}(I\prod I',\,I,\,\mathrm{Prod.fst})\;p = \langle p\!\!.proj.1,\; p\!\!.2.1\rangle$$$

Lean4

@[simp, mfld_simps]
theorem mfderiv_fst {x : M × M'} :
    mfderiv (I.prod I') I Prod.fst x = ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2) :=
  (hasMFDerivAt_fst x).mfderiv

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