toTopologicalSpace — Mathlib

English

The topological structure on the total space is inherited from the fiber bundle core, ensuring continuity of local trivializations.

Русский

Топологическая структура полного пространства наследуется от ядра фиброблока, обеспечивая непрерывность локальных тривиализаций.

LaTeX

$$$Z.TotalSpace$ carries the topology induced by $Z.toFiberBundleCore.toTopologicalSpace$$$

Lean4

/-- Topological structure on the total space of a vector bundle created from core, designed so
that all the local trivialization are continuous. -/
instance toTopologicalSpace : TopologicalSpace Z.TotalSpace :=
  Z.toFiberBundleCore.toTopologicalSpace

Похожие утверждения