not_firstCountableTopology_opc

Mathlib.Topology.Instances.RatLemmas

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

English

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

Русский

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

LaTeX

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

Lean4

theorem not_firstCountableTopology_opc : ¬FirstCountableTopology ℚ∞ :=
  by
  intro
  exact not_countably_generated_nhds_infty_opc inferInstance

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

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

Разделы

Аффилиация

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