toFirstCountable

Mathlib.Topology.AlexandrovDiscrete

URI: https://scilib.ai/kg/mathlib#AlexandrovDiscrete.toFirstCountable

English

Every Alexandrov-discrete space is locally countable, i.e., locally has a countable neighborhood basis.

Русский

Каждое пространство Александрово-дискретное локально счетно у базах окрестностей.

LaTeX

$$FirstCountableTopology α$$

Lean4

instance toFirstCountable : FirstCountableTopology α where
  nhds_generated_countable a := ⟨{nhdsKer { a }}, countable_singleton _, by simp⟩

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

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

Разделы

Аффилиация

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