trivializationAt_target — Mathlib

English

For every point x in the manifold, the target of the tangent bundle trivialization at x is the product of the chart source at x with the full fiber; i.e., it equals (chartAt H x).source × univ.

Русский

Для каждой точки x на многообразии целевая часть тривиализации касательного пространства в точке x равна произведению области определения чарта в x на всё волокно; то есть она равна (chartAt H x).source × univ.

LaTeX

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

Lean4

@[simp, mfld_simps]
theorem trivializationAt_target (x : M) :
    (trivializationAt E (TangentSpace I) x).target = (chartAt H x).source ×ˢ univ :=
  rfl

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