English
Let x be a point of M. Then the chart at x, viewed as a map from M to H, is differentiable in the sense of MDifferentiable from I to I (i.e., chartAt(H, x) is differentiable with respect to the given model I).
Русский
Пусть x принадлежит M. Тогда карта chartAt(H, x), рассматриваемая как отображение M → H, дифференцируема в смысле MDifferentiable от I к I (то есть chartAt(H, x) дифференцируема относительно заданной модели I).
LaTeX
$$$\mathrm{MDifferentiable}(I,I,\mathrm{chartAt}(H,x))$$$
Lean4
theorem mdifferentiable_chart (x : M) : (chartAt H x).MDifferentiable I I :=
mdifferentiable_of_mem_atlas (chart_mem_atlas _ _)