isLindelof_empty

Mathlib.Topology.Compactness.Lindelof

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

← MathLib Explorer

English

The empty set is Lindelöf.

Русский

Пустое множество является Линдельёфовым.

LaTeX

$$$IsLindelof(\emptyset).$$$

Lean4

/-- The empty set is a Lindelof set. -/
@[simp]
theorem isLindelof_empty : IsLindelof (∅ : Set X) := fun _f hnf _ hsf ↦
  Not.elim hnf.ne <| empty_mem_iff_bot.1 <| le_principal_iff.1 hsf

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

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

Разделы

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

Аффилиация

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