English
For a set s and point x in s, the MF-derivative within s of Prod.fst is the fst-linear map on the tangent spaces, i.e. mfderivWithin (I.prod I′) I Prod.fst s x = ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2).
Русский
Внутренняя производная MF для Prod.fst по множеству s равна fst-оператору между касательными пространствами.
LaTeX
$$$mfderivWithin (I\prod I')\, I\, Prod.fst\, s\, x = \mathrm{ContinuousLinearMap.fst}\; 𝕜\; (\mathrm{TangentSpace}\; I\, x.1)\; (\mathrm{TangentSpace}\; I'\, x.2)$$$
Lean4
theorem tangentMapWithin_prodFst {s : Set (M × M')} {p : TangentBundle (I.prod I') (M × M')}
(hs : UniqueMDiffWithinAt (I.prod I') s p.proj) : tangentMapWithin (I.prod I') I Prod.fst s p = ⟨p.proj.1, p.2.1⟩ :=
by
simp only [tangentMapWithin]
rw [mfderivWithin_fst]
· rcases p with ⟨⟩; rfl
· exact hs
