countable_countableBasis

Mathlib.Topology.Bases

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.countable_countableBasis

English

If α is a second-countable space, then the countableBasis α is countable.

Русский

Если α является пространством с второй счётностью, то countableBasis α счётна.

LaTeX

$$$(countableBasis\,\alpha).Countable$$$

Lean4

theorem countable_countableBasis [SecondCountableTopology α] : (countableBasis α).Countable :=
  (exists_countable_basis α).choose_spec.1

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

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

Разделы

Аффилиация

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