English
Let M and M′ be charted spaces with charts I and I′. The projection map from the product M × M′ to M, given by fst(m, m′) = m, is differentiable in the MF-sense on every subset s, i.e. MDifferentiableWithinAt (I.prod I′) I Prod.fst s x for all s ⊆ M × M′ and all x ∈ s.
Русский
Пусть M и M′ — хлитированные пространства с картами I и I′. Отображение проекции из произведения M × M′ на M, заданное fst(m, m′) = m, дифференцируемо в смысле MF на любой подмножество s, то есть MDifferentiableWithinAt (I.prod I′) I Prod.fst s x для всех s и x ∈ s.
LaTeX
$$$\mathrm{MDifferentiableWithinAt}(I\times I',\,I,\,\mathrm{Prod.fst},\,s,\,x)$$$
Lean4
theorem mdifferentiableWithinAt_fst {s : Set (M × M')} {x : M × M'} :
MDifferentiableWithinAt (I.prod I') I Prod.fst s x :=
mdifferentiableAt_fst.mdifferentiableWithinAt
