hasColimits — Mathlib

English

The category of compact Hausdorff spaces has all colimits; these are created by the reflective functor to Top.

Русский

Категория компактных хаусдорфовых пространств имеет все колимиты; они создаются отражающим функтором в Top.

LaTeX

$$$\mathbf{HasColimits}(\mathbf{CompHaus})$$$

Lean4

instance hasColimits : Limits.HasColimits CompHaus :=
  hasColimits_of_reflective compHausToTop

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