tangentMap_proj

Mathlib.Geometry.Manifold.MFDeriv.Basic

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

English

The tangent map (global) satisfies the same projection equality.

Русский

Глобальная касательная карта удовлетворяет тем же равенствам проекции.

LaTeX

$$$$ (tangentMap I I' f p).proj = f p.proj $$$$

Lean4

@[simp, mfld_simps]
theorem tangentMap_proj {p : TangentBundle I M} : (tangentMap I I' f p).proj = f p.proj :=
  rfl

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

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

Разделы

Аффилиация

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