instUCompactlyGeneratedSpaceCarrierObjTopCatCondensedSetToTopCat

English

For X a condensed set, the carrier of condensedSetToTopCat.obj X is a UCompactlyGeneratedSpace.

Русский

Для конденсированного множества X носитель condensedSetToTopCat.obj X является пространством с характеристикой UCompactlyGenerated.

LaTeX

$$$\mathrm{UCompactlyGeneratedSpace}(\mathrm{condensedSetToTopCat.obj}(X).\mathrm{carrier})$$$

Lean4

instance (X : CondensedSet.{u}) : UCompactlyGeneratedSpace.{u, u + 1} (condensedSetToTopCat.obj X) :=
  inferInstanceAs (UCompactlyGeneratedSpace.{u, u + 1} X.toTopCat)

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