instTopologicalSpaceTangentBundle

English

The tangent coordinate change is defined as the derivative of the coordinate-change map between two charts.

Русский

Переход касательных координат задан как производная перехода координат между двумя диаграммами.

LaTeX

$$$$ \mathrm{tangentCoordChange} I x y z = fderivWithin 𝕜 (extChartAt I y ∘ (extChartAt I x).symm) (range I) (extChartAt I x z) $$$$

Lean4

instance : TopologicalSpace TM :=
  (tangentBundleCore I M).toTopologicalSpace

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