mfderivWithin_snd — Mathlib

English

For any tangent bundle element p on the product, the tangent map of Prod.fst yields the pair consisting of the first component of p and the first component of the second factor: ⟨p.proj.1, p.2.1⟩.

Русский

Для касательного вектора p на произведении касательных отображение tangentMapProdFst дает пару ⟨p.proj.1, p.2.1⟩.

LaTeX

$$$tangentMap\_prodFst\;p = \langle p.proj.1, p.2.1 \rangle$$$

Lean4

theorem mfderivWithin_snd {s : Set (M × M')} {x : M × M'} (hxs : UniqueMDiffWithinAt (I.prod I') s x) :
    mfderivWithin (I.prod I') I' Prod.snd s x = ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2) :=
  by rw [MDifferentiable.mfderivWithin mdifferentiableAt_snd hxs]; exact mfderiv_snd

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