isLindelof_singleton

Mathlib.Topology.Compactness.Lindelof

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

← MathLib Explorer

English

A singleton set is Lindelöf.

Русский

Один элемент образует Линдельёфово множество.

LaTeX

$$$IsLindelof(\{x\})$ for any x.$$

Lean4

/-- A singleton set is a Lindelof set. -/
@[simp]
theorem isLindelof_singleton {x : X} : IsLindelof ({ x } : Set X) := fun _ hf _ hfa ↦
  ⟨x, rfl, ClusterPt.of_le_nhds' (hfa.trans <| by simpa only [principal_singleton] using pure_le_nhds x) hf⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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