toRiemannianMetric — Mathlib

English

From a smooth Riemannian metric, obtain a (classical) Riemannian metric on the bundle.

Русский

Из гладкой римановой метрики получаем обычную риманову метрику на расслоении.

LaTeX

$$def toRiemannianMetric (g : ContMDiffRiemannianMetric IB n F E) : RiemannianMetric E$$

Lean4

/-- A smooth Riemannian metric defines in particular a Riemannian metric. -/
def toRiemannianMetric (g : ContMDiffRiemannianMetric IB n F E) : RiemannianMetric E :=
  g.toContinuousRiemannianMetric.toRiemannianMetric

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