tangentBundleCore_localTriv_baseSet

English

Changing from a chart to itself yields the identity on the fiber direction: tanCoordChange I x x z v = v.

Русский

Переход координат от диаграммы к самой диаграмме по касательному направлению действует как тождественный на v: tangentCoordChange I x x z v = v.

LaTeX

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

Lean4

@[simp]
theorem tangentBundleCore_localTriv_baseSet (i) : ((tangentBundleCore I M).localTriv i).baseSet = i.1.source :=
  rfl

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