Second countability of fibre bundles

A fibre bundle with second-countable base and model fibre has second-countable total space. This allows metrizability results for manifolds to apply to finite-dimensional vector bundles, including normal bundles. Over a second-countable base, countably many of the preferred trivializations trivializationAt cover the base (TauCeti.FiberBundle.exists_iUnion_baseSet_trivializationAt_eq_univ); this is how measurability of sections is tested chart by chart.

instance TauCeti.FiberBundle.secondCountableTopology_totalSpace {B : Type u_1} {F : Type u_2} {V : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [SecondCountableTopology B] [SecondCountableTopology F] : SecondCountableTopology (Bundle.TotalSpace F V)

A fibre bundle with second-countable base and model fibre has second-countable total space.

theorem TauCeti.FiberBundle.exists_iUnion_baseSet_trivializationAt_eq_univ (F : Type u_1) {B : Type u_2} (V : B → Type u_3) [TopologicalSpace B] [TopologicalSpace F] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [SecondCountableTopology B] [Nonempty B] : ∃ (p : ℕ → B), ⋃ (n : ℕ), (trivializationAt F V (p n)).baseSet = Set.univ

Over a nonempty second-countable base, the base sets of countably many preferred trivializations trivializationAt F V (p n) cover the base.