isCompact_singleton

Mathlib.Topology.Compactness.Compact

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

← MathLib Explorer

English

A singleton set is compact.

Русский

Одиночное множество компактно.

LaTeX

$$$\\{x\\} \\text{ is compact}$$$

Lean4

theorem isCompact_singleton {x : X} : IsCompact ({ 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