English
The total space is endowed with a topology generated by the open sets that come from all local trivializations: unions of source intersections with preimages of open sets in B × F under the local trivializations.
Русский
Общее пространство оснащено топологией, порождаемой открытыми множествами, возникающими из всех локальных тривиализаций: объединения источников, пересечённых с обратимыми образами открытых множеств в B × F по локальным тривиализациям.
LaTeX
$$$\\text{ToTopologicalSpace}(Z):=\\text{TopSpace.generateFrom} \\Big(\\bigcup_{i,s}\\, \\{ \\mathrm{source}(\\mathcal{L}_i) \\cap \\mathcal{L}_i^{-1}[s] \\} \\Big)$$$
Lean4
/-- Topological structure on the total space of a fiber bundle created from core, designed so
that all the local trivialization are continuous. -/
instance toTopologicalSpace : TopologicalSpace (Bundle.TotalSpace F Z.Fiber) :=
TopologicalSpace.generateFrom <|
⋃ (i : ι) (s : Set (B × F)) (_ : IsOpen s),
{(Z.localTrivAsPartialEquiv i).source ∩ Z.localTrivAsPartialEquiv i ⁻¹' s}
