topologicalSpace — Mathlib

English

The total space topology for a trivial bundle is given by the infimum of the pullback topologies from base and fiber.

Русский

Топология полного пространства тривиального расслоения задаётся инфимином (меньшей границей) топологий на основании и волокне.

LaTeX

$$$ \text{TopSpace}(TotalSpace F (Trivial B F)) = \operatorname{induced}(TotalSpace.proj, t_B) \; \infimum \; \operatorname{induced}(TotalSpace.trivialSnd B F, t_F) $$$

Lean4

instance topologicalSpace [t₁ : TopologicalSpace B] [t₂ : TopologicalSpace F] :
    TopologicalSpace (TotalSpace F (Trivial B F)) :=
  induced TotalSpace.proj t₁ ⊓ induced (TotalSpace.trivialSnd B F) t₂

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