tangentMap_id

Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

URI: https://scilib.ai/kg/mathlib#tangentMap_id

English

The tangent map of the identity map is the identity on the tangent bundle.

Русский

Касательное отображение тождественной карты равно тождественному отображению на касательном каскаде.

LaTeX

$$$ tangentMap I I (id : M \to M) = id $$$

Lean4

@[simp, mfld_simps]
theorem tangentMap_id : tangentMap I I (id : M → M) = id := by ext1 ⟨x, v⟩; simp [tangentMap]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru