NatUnionInfty

Mathlib.Topology.Category.LightProfinite.Sequence

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

Lean4

/-- The one point compactification of the natural numbers as a light profinite set. -/
abbrev NatUnionInfty : LightProfinite :=
  of (OnePoint ℕ)

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

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

Разделы

Аффилиация

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