English
The total space topology of a FiberPrebundle is defined as the supremum over all pretrivializations in its atlas of the coinduced topologies on their targets.
Русский
Топология полного пространства предрасслоения задаётся как верхняя граница (предел) по всем предтривиализациям в атласе, применённая к их целям через когениированные топологии.
LaTeX
$$$ \text{TotalSpaceTopology}(a) = \bigvee_{e \in a.pretrivializationAtlas} \; \operatorname{coinduced}(e.setSymm, \operatorname{TopologicalSpaceSubtype}) $$$
Lean4
/-- Topology on the total space that will make the prebundle into a bundle. -/
def totalSpaceTopology (a : FiberPrebundle F E) : TopologicalSpace (TotalSpace F E) :=
⨆ (e : Pretrivialization F (π F E)) (_ : e ∈ a.pretrivializationAtlas),
coinduced e.setSymm instTopologicalSpaceSubtype
