English
If a continuous Riemannian metric g on F E is used to define g.toRiemannianMetric, then the bundle E with this induced metric is a continuous Riemannian bundle; i.e., IsContinuousRiemannianBundle F E holds.
Русский
Если единственный непрерывный риманов метрический g на F→E применяется к определению g.toRiemannianMetric, то волокно E с полученной метрикой образует непрерывную риманову связку.
LaTeX
$$$$IsContinuousRiemannianBundle\ F\ E\; \text{ holds when } g\text{ is a }\text{ContinuousRiemannianMetric on }F\to E.$$$$
Lean4
/-- If a Riemannian bundle structure is defined using `g.toRiemannianMetric` where `g` is
a `ContinuousRiemannianMetric`, then we make sure typeclass inference can infer automatically
that the bundle is a continuous Riemannian bundle. -/
instance (g : ContinuousRiemannianMetric F E) :
letI : RiemannianBundle E := ⟨g.toRiemannianMetric⟩;
IsContinuousRiemannianBundle F E :=
by
letI : RiemannianBundle E := ⟨g.toRiemannianMetric⟩
exact ⟨⟨g.inner, g.continuous, fun b v w ↦ rfl⟩⟩
