Finite-rank vector bundles #
theorem
VectorBundle.finiteDimensional
(R : Type u_1)
{B : Type u_2}
(F : Type u_3)
(E : B → Type u_4)
[NontriviallyNormedField R]
[TopologicalSpace B]
[TopologicalSpace (Bundle.TotalSpace F E)]
[NormedAddCommGroup F]
[NormedSpace R F]
[(x : B) → TopologicalSpace (E x)]
[FiberBundle F E]
[(x : B) → AddCommGroup (E x)]
[(x : B) → Module R (E x)]
[VectorBundle R F E]
(b : B)
[FiniteDimensional R F]
:
FiniteDimensional R (E b)
theorem
VectorBundle.finrank_eq
(R : Type u_1)
{B : Type u_2}
(F : Type u_3)
(E : B → Type u_4)
[NontriviallyNormedField R]
[TopologicalSpace B]
[TopologicalSpace (Bundle.TotalSpace F E)]
[NormedAddCommGroup F]
[NormedSpace R F]
[(x : B) → TopologicalSpace (E x)]
[FiberBundle F E]
[(x : B) → AddCommGroup (E x)]
[(x : B) → Module R (E x)]
[VectorBundle R F E]
(b : B)
: