instRiemannianBundleTangentSpaceRealModelWithCornersSelf

English

The tangent bundle to a real vector space F, endowed with the standard inner product on each tangent space, forms a natural Riemannian bundle.

Русский

Касательное расслоение к вещественному пространству F, снабжённое стандартным скалярным произведением на каждой касательной, образует естественное римманово расслоение.

LaTeX

$$$$T F\\text{ carries the natural Riemannian metric }g_x(v,w)=\\langle v,w\\rangle\\text{ on each }T_xF.$$$$

Lean4

noncomputable instance : RiemannianBundle (fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x) :=
  ⟨(riemannianMetricVectorSpace F).toRiemannianMetric⟩

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