symmL_model_space — Mathlib

English

If I is a manifold of dimension (n+1) on M, then TangentBundle defines a ContMDiffVectorBundle of index n, E, over TangentSpace I with structure I.

Русский

Если I задаёт многообразие размерности (n+1) на M, то TangentBundle определяет ContMDiffVectorBundle индексом n над TangentSpace I с данной структурой I.

LaTeX

$$$\text{ContMDiffVectorBundle } n\; E\; (\mathrm{TangentSpace}\;I)\ I$$$

Lean4

@[simp high, mfld_simps]
theorem symmL_model_space (b b' : F) : (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b).symmL 𝕜 b' = (1 : F →L[𝕜] F) :=
  by
  rw [TangentBundle.symmL_trivializationAt_eq_core, coordChange_model_space]
  apply mem_univ

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