English
Continuity of the total space injections extends to the total space topology of the prebundle, yielding a coherent fiber bundle structure.
Русский
Непрерывность включения полного пространства распространяется на топологию полного пространства предрасслоения, образуя согласованную структуру фибер-бандла.
LaTeX
$$$ \forall b : B,\; \text{Continuous}(\mathrm{TotalSpace.mk}\, b) $$$
Lean4
@[continuity]
theorem continuous_totalSpaceMk (b : B) : Continuous[_, a.totalSpaceTopology] (TotalSpace.mk b) :=
by
letI := a.totalSpaceTopology
let e := a.trivializationOfMemPretrivializationAtlas (a.pretrivialization_mem_atlas b)
rw [e.toOpenPartialHomeomorph.continuous_iff_continuous_comp_left (a.totalSpaceMk_preimage_source b)]
exact continuous_iff_le_induced.2 (a.totalSpaceMk_isInducing b).eq_induced.le
