tangentCoordChange_self — Mathlib

English

Again, in the self-chart case, the tangent coordinate change acts as the identity on vectors.

Русский

В случае самопереноса диаграммы переход касательных координат действует как тождество на векторах.

LaTeX

$$$$ (\mathrm{tangentCoordChange} I x x z)(v) = v $$$$

Lean4

theorem tangentCoordChange_self {x z : M} {v : E} (h : z ∈ (extChartAt I x).source) :
    tangentCoordChange I x x z v = v :=
  by
  apply (tangentBundleCore I M).coordChange_self
  rw [tangentBundleCore_baseSet, coe_achart, ← extChartAt_source I]
  exact h

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