instSecondCountableTopologyCarrierToTopAndTotallyDisconnectedSpace

Mathlib.Topology.Category.LightProfinite.Basic

URI: https://scilib.ai/kg/mathlib#LightProfinite.instSecondCountableTopologyCarrierToTopAndTotallyDisconnectedSpace

English

Every LightProfinite X carries a second countable topology on its underlying carrier space.

Русский

У каждого LightProfinite X топология на носители X вторичного счёта (second countable).

LaTeX

$$$\text{SecondCountableTopology}(X)$$$

Lean4

instance {X : LightProfinite} : SecondCountableTopology X :=
  X.prop.2

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

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

Разделы

Аффилиация

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