English
A fibre in a bundle with a Riemannian bundle structure inherits a NormedAddCommGroup structure on each fibre E_b. The norm is induced by the fibre inner product: for v ∈ E_b, define ∥v∥_b := sqrt(⟨v,v⟩_b).
Русский
Волокно с римановской структурой на волокнах имеет на каждом волокне E_b нормированную аддитивную коммутативную группу, норму задаём через скалярное произведение: ∥v∥_b := sqrt(⟨v,v⟩_b).
LaTeX
$$$$\|v\|_b := \sqrt{\langle v,v\rangle_b},\quad v\in E_b,\quad \text{(E_b, ∥·∥_b) is a NormedAddCommGroup.}$$$$
Lean4
/-- A fiber in a bundle satisfying the `[RiemannianBundle E]` typeclass inherits
a `NormedAddCommGroup` 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) : NormedAddCommGroup (E b) :=
(h.g.toCore b).toNormedAddCommGroupOfTopology (h.g.continuousAt b) (h.g.isVonNBounded b)
