instCompactSpaceCarrierObjTopCatCompHausLikeToTop

Mathlib.Topology.Category.CompHausLike.Basic

URI: https://scilib.ai/kg/mathlib#CompHausLike.instCompactSpaceCarrierObjTopCatCompHausLikeToTop

English

The carrier of a CompHausLike object carries a compact topology.

Русский

Носитель объекта CompHausLike несет компактную топологию.

LaTeX

$$$\text{CompactSpace}((\mathrm{compHausLikeToTop}~P).\mathrm{obj} X).\mathrm{carrier}$$$

Lean4

instance (X : CompHausLike P) : CompactSpace ((compHausLikeToTop P).obj X) :=
  inferInstanceAs (CompactSpace X.toTop)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru