isLindelof_diagonal

Mathlib.Topology.Compactness.Lindelof

URI: https://scilib.ai/kg/mathlib#isLindelof_diagonal

English

The diagonal subspace of a Lindelöf space is Lindelöf.

Русский

Диагональ пространства Линдельфово.

LaTeX

$$$[LindelofSpace X] \Rightarrow IsLindelof (diagonal X)$$$

Lean4

theorem isLindelof_diagonal [LindelofSpace X] : IsLindelof (diagonal X) :=
  @range_diag X ▸ isLindelof_range (continuous_id.prodMk continuous_id)

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

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

Разделы

Аффилиация

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