trivializationAt_baseSet — Mathlib

English

For the tangent bundle trivialization at x, the base set equals the chart source at x; i.e., (trivializationAt E (TangentSpace I) x).baseSet = (chartAt H x).source.

Русский

Для тривиализации касательного пространства в точке x базовый набор равен области определения чарта в x; то есть baseSet тривиализации равен source чарта.

LaTeX

$$$\big(\mathrm{trivializationAt}\,E\,(\mathrm{TangentSpace}\,I)\;x\big).\mathrm{baseSet} = (\mathrm{chartAt}\;H\;x).\mathrm{source}$$$

Lean4

@[simp, mfld_simps]
theorem trivializationAt_baseSet (x : M) : (trivializationAt E (TangentSpace I) x).baseSet = (chartAt H x).source :=
  rfl

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