tangentBundleCore_baseSet — Mathlib

English

The coordChange field of tangentBundleCore with charts x,y is the derivative of the coordinate change map between extChartAt I x and extChartAt I y.

Русский

Поле coordChange у tangentBundleCore для диаграмм x,y равно производной перехода координат между extChartAt I x и extChartAt I y.

LaTeX

$$$$ (tangentBundleCore I M).coordChange (\mathrm{achart} H x) (\mathrm{achart} H y) z = fderivWithin 𝕜 (extChartAt I y ∘ (extChartAt I x).symm) (range I) (extChartAt I x z). $$$$

Lean4

/-- `simp`-normal form is `tangentBundleCore_localTriv_baseSet`. -/
theorem tangentBundleCore_baseSet (i) : (tangentBundleCore I M).baseSet i = i.1.source :=
  rfl

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