not_secondCountableTopology_opc

Mathlib.Topology.Instances.RatLemmas

URI: https://scilib.ai/kg/mathlib#Rat.not_secondCountableTopology_opc

English

The one-point compactification of the rationals is not second countable.

Русский

Одноточечное компактирование ℚ не обладает вторым счётным свойством.

LaTeX

$$$\neg\operatorname{SecondCountableTopology}(\mathbb{Q}_{\infty})$$$

Lean4

theorem not_secondCountableTopology_opc : ¬SecondCountableTopology ℚ∞ :=
  by
  intro
  exact not_firstCountableTopology_opc inferInstance

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

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

Разделы

Аффилиация

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