topologicalSpaceCoconePtOfCoconeForget

English

The topology on the cocone point of a cocone forgetful to TopCat is defined as the supremum over j of the coinduced topologies via the cocone maps.

Русский

Топология на точке кокона кокона, забывающего в TopCat, задаётся как наибольшая (супремум) из коиндуцированных топологий через карты кокона.

LaTeX

$$$ \text{TopCat.topologicalSpaceCoconePtOfCoconeForget}(F,c) = \bigvee_j (F.obj j).str.coinduced (c.ι.app j) $$$

Lean4

instance topologicalSpaceCoconePtOfCoconeForget : TopologicalSpace (coconePtOfCoconeForget c) :=
  (⨆ j, (F.obj j).str.coinduced (c.ι.app j))

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