topologicalSpaceConePtOfConeForget

English

In a diagram of TopCat cones, the topology on the cone point is the infimum of the induced topologies via the cone maps.

Русский

В диаграмме конусов TopCat топология на вершине конуса равна наименьшей топологии, порождённой отображениями конуса.

LaTeX

$$$\\mathrm{TopCat}.topologicalSpaceConePtOfConeForget(c) = \\bigwedge_j (F(j).\\mathrm{str}.induced (c.\\pi.app j))$$$

Lean4

instance topologicalSpaceConePtOfConeForget : TopologicalSpace (conePtOfConeForget c) :=
  (⨅ j, (F.obj j).str.induced (c.π.app j))

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