English
If a function is differentiable at p and the tangent structure near p is unique, then the tangent map within s equals the tangent map on the whole space at p.
Русский
Если функция дифференцируема в точке p и в окрестности p уникальна касательная структура, то касательная карта внутри s совпадает с касательной картой на всём пространстве в p.
LaTeX
$$$$UniqueMDiffWithinAt I s p.1 \\land MDifferentiableAt I I' f p.1 \\rightarrow tangentMapWithin I I' f s p = tangentMap I I' f p$$$$
Lean4
theorem tangentMapWithin_subset {p : TangentBundle I M} (st : s ⊆ t) (hs : UniqueMDiffWithinAt I s p.1)
(h : MDifferentiableWithinAt I I' f t p.1) : tangentMapWithin I I' f s p = tangentMapWithin I I' f t p :=
by
simp only [tangentMapWithin, mfld_simps]
rw [mfderivWithin_subset st hs h]
