instSequentialSpaceCarrierToTopCat

Mathlib.Condensed.Light.TopCatAdjunction

URI: https://scilib.ai/kg/mathlib#LightCondSet.instSequentialSpaceCarrierToTopCat

English

The carrier of LightCondSet.toTopCat is a sequential space.

Русский

Носитель LightCondSet.toTopCat обладает последовательной топологией.

LaTeX

$$$\operatorname{SequentialSpace}\left((\text{LightCondSet}.toTopCat)\text{.carrier}\right)$$$

Lean4

instance (X : LightCondSet.{u}) : SequentialSpace X.toTopCat := by apply SequentialSpace.coinduced

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

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

Разделы

Аффилиация

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