tangentMap_prodFst — Mathlib

English

The MF-derivative of the first projection equals the fst-linear map between the tangent spaces: mfderiv (I.prod I′) I Prod.fst x = ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I′ x.2).

Русский

Производная MF для первой проекции равна линейному отображению fst между касательными пространствами.

LaTeX

$$$mfderiv (I\cdot I')\, I\, Prod.fst\, x = \mathrm{ContinuousLinearMap.fst}\; 𝕜\; (\mathrm{TangentSpace}\; I\, x.1)\; (\mathrm{TangentSpace}\; I'\, x.2)$$$

Lean4

@[simp, mfld_simps]
theorem tangentMap_prodFst {p : TangentBundle (I.prod I') (M × M')} :
    tangentMap (I.prod I') I Prod.fst p = ⟨p.proj.1, p.2.1⟩ := by simp [tangentMap]; rfl

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