isLindelof

Mathlib.Topology.Compactness.Lindelof

URI: https://scilib.ai/kg/mathlib#Set.Subsingleton.isLindelof

English

If a set is subsingleton, it is Lindelöf.

Русский

Если множество состоит из не более одной точки, оно Линдельёфово.

LaTeX

$$$s \text{ is Subsingleton} \Rightarrow IsLindelof(s).$$$

Lean4

theorem isLindelof (hs : s.Subsingleton) : IsLindelof s :=
  Subsingleton.induction_on hs isLindelof_empty fun _ ↦ isLindelof_singleton

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

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

Разделы

Аффилиация

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