isSigmaCompact_empty

Mathlib.Topology.Compactness.SigmaCompact

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

English

The empty set is σ-compact.

Русский

Пустое множество является σ-компактным.

LaTeX

$$$\text{IsSigmaCompact}(\emptyset)$$$

Lean4

/-- The empty set is σ-compact. -/
@[simp]
theorem isSigmaCompact_empty : IsSigmaCompact (∅ : Set X) :=
  IsCompact.isSigmaCompact isCompact_empty

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

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

Разделы

Аффилиация

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