mfderivWithin_id — Mathlib

English

Within a set s, the derivative of the identity map is the identity on the tangent space, provided a suitable non-degeneracy condition holds.

Русский

Внутри множества s производная тождественного отображения равна тождественному линейному отображению на касательном пространстве при выполнении соответствующего условия непрерывности внутри.

LaTeX

$$$ mfderivWithin I I (@id M) s x = \mathrm{Id}_{\mathrm{TangentSpace} I x}$$$

Lean4

theorem mfderivWithin_id (hxs : UniqueMDiffWithinAt I s x) :
    mfderivWithin I I (@id M) s x = ContinuousLinearMap.id 𝕜 (TangentSpace I x) :=
  by
  rw [MDifferentiable.mfderivWithin mdifferentiableAt_id hxs]
  exact mfderiv_id

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