toContinuousRiemannianMetric — Mathlib

English

A smooth Riemannian metric on a vector bundle induces a continuous Riemannian metric on the same bundle.

Русский

Гладкая риманова метрика на векто-расслоении порождает непрерывную риманову метрику на том же расслоении.

LaTeX

$$def toContinuousRiemannianMetric (g : ContMDiffRiemannianMetric IB n F E) : ContinuousRiemannianMetric F E$$

Lean4

/-- A smooth Riemannian metric defines in particular a continuous Riemannian metric. -/
def toContinuousRiemannianMetric (g : ContMDiffRiemannianMetric IB n F E) : ContinuousRiemannianMetric F E :=
  { g with continuous := g.contMDiff.continuous }

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