mdifferentiable_chart — Mathlib

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 _ _)

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