topologicalSpace — Mathlib

English

The pullback topology is equal to the canonical pullback topology defined via the construction.

Русский

Топология pullback равна канонической топологии pullback, определяемой через конструкцию.

LaTeX

$$$\mathrm{pullbackTopology\ F\ E\ f} = \mathrm{Pullback.TotalSpace.topologicalSpace}\ F\ E\ f$$$

Lean4

/-- The topology on the total space of a pullback bundle is the coarsest topology for which both
the projections to the base and the map to the original bundle are continuous. -/
instance topologicalSpace : TopologicalSpace (TotalSpace F (f *ᵖ E)) :=
  pullbackTopology F E f

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