English
For every fibre E_b there is an inner product space structure, given by ⟨v,w⟩_b := g.inner b v w, where g is a Riemannian metric on the fibres.
Русский
Для каждого волокна E_b существует структура пространства с внутренним произведением, задаваемая ⟨v,w⟩_b := g.inner b v w, где g — риманова метрика на волокнах.
LaTeX
$$$$\langle v,w\rangle_b := g.inner b v w,\quad v,w\in E_b,$$$$
Lean4
/-- A fiber in a bundle satisfying the `[RiemannianBundle E]` typeclass inherits
an `InnerProductSpace ℝ` structure.
The normal priority for an instance which always applies like this one should be 100.
We use 80 as this is rather specialized, so we want other paths to be tried first typically.
As this instance is quite specific and very costly because of higher-order unification, we
also scope it to the `Bundle` namespace. -/
noncomputable scoped instance (priority := 80) [h : RiemannianBundle E] (b : B) : InnerProductSpace ℝ (E b) :=
.ofCoreOfTopology (h.g.toCore b) (h.g.continuousAt b) (h.g.isVonNBounded b)
