trivializationAt_fst — Mathlib

English

The first component of the trivialization at x of the tangent bundle is simply the base point; i.e., (trivializationAt E (TangentSpace I) x z).1 = z.1.

Русский

Первая компонента тривиализации в точке x касательного пространства равна базовой точке: (trivializationAt E (TangentSpace I) x z).1 = z.1.

LaTeX

$$$((\mathrm{trivializationAt}\,E\,(\mathrm{TangentSpace}\,I)\;x\;z)).1 = z.1$$$

Lean4

@[simp, mfld_simps]
theorem trivializationAt_fst (x : M) (z : TM) : (trivializationAt E (TangentSpace I) x z).1 = z.1 :=
  rfl

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