hasMFDerivWithinAt_id — Mathlib

English

The MF-derivative within at x of the identity map on a charted space is the identity's derivative.

Русский

MF-производная внутри для тождественного отображения на пространстве сетки равно дифференцированию тождества.

LaTeX

$$hasMFDerivWithinAt_id (s : Set M) (x : M) : HasMFDerivWithinAt I I (@id M) s x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))$$

Lean4

theorem hasMFDerivWithinAt_id (s : Set M) (x : M) :
    HasMFDerivWithinAt I I (@id M) s x (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) :=
  (hasMFDerivAt_id x).hasMFDerivWithinAt

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