union

Mathlib.Topology.Compactness.Lindelof

URI: https://scilib.ai/kg/mathlib#IsLindelof.union

← MathLib Explorer

English

If s and t are Lindelöf, then their union s ∪ t is Lindelöf.

Русский

Если s и t — Линдельоф, то их объединение s ∪ t — Линдельоф.

LaTeX

$$$IsLindelof\,s \rightarrow IsLindelof\,t \rightarrow IsLindelof\,(s \cup t)$$$

Lean4

theorem union (hs : IsLindelof s) (ht : IsLindelof t) : IsLindelof (s ∪ t) := by rw [union_eq_iUnion];
  exact isLindelof_iUnion fun b => by cases b <;> assumption

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

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

Разделы

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

Аффилиация

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