Hausdorffness of the total space of a fiber bundle

Mathlib records that each fiber of a fiber bundle inherits the separation axioms of the model fiber (FiberBundle.t2Space). This file proves the corresponding statement for the total space: if the base and the model fiber are Hausdorff, so is the total space.

Two points of the total space over distinct base points are separated by preimages under the projection. Two points over the same base point lie in the source of one local trivialization, which is a homeomorphism onto an open subset of the Hausdorff space B × F.

The main application is to tangent bundles: the tangent bundle of a Hausdorff manifold is Hausdorff, which is what uniqueness of integral curves of vector fields on the tangent bundle, such as the geodesic spray, requires.

instance TauCeti.FiberBundle.t2Space_totalSpace {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] [T2Space B] [T2Space F] : T2Space (Bundle.TotalSpace F E)

The total space of a fiber bundle with Hausdorff base and Hausdorff model fiber is Hausdorff.