mfderiv_id — Mathlib

English

Let M be a charted space with tangent spaces. The derivative of the identity map at x is the identity on the tangent space at x.

Русский

Пусть M — многообразие с диаграммой; касательное пространство к точке x обозначим T_xM. Производная тождественного отображения в точке x есть тождественное отображение на касательном пространстве.

LaTeX

$$$ mfderiv I I (\mathrm{id}_M)\ x = \mathrm{Id}_{\mathrm{TangentSpace} I x}$$$

Lean4

@[simp, mfld_simps]
theorem mfderiv_id : mfderiv I I (@id M) x = ContinuousLinearMap.id 𝕜 (TangentSpace I x) :=
  HasMFDerivAt.mfderiv (hasMFDerivAt_id x)

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