tangentMapWithin_id — Mathlib

English

The tangent map within the identity on M is the identity on the tangent bundle restricted to a subset p.

Русский

Касательное отображение внутри тождества на M acts как тождественная карта на касательном пространстве для точки p.

LaTeX

$$$ tangentMapWithin I I (id : M \to M) s p = p $$$

Lean4

theorem tangentMapWithin_id {p : TangentBundle I M} (hs : UniqueMDiffWithinAt I s p.proj) :
    tangentMapWithin I I (id : M → M) s p = p :=
  by
  simp only [tangentMapWithin, id]
  rw [mfderivWithin_id]
  · rcases p with ⟨⟩; rfl
  · exact hs

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