isClopen_sUnion

Mathlib.Topology.AlexandrovDiscrete

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

← MathLib Explorer

English

The union of a family of clopen sets is clopen.

Русский

Объединение семейства clopen множеств является clopen.

LaTeX

$$$\forall S:\text{Set}(\text{Set}(\alpha)), (\forall s\in S, IsClopen(s)) \Rightarrow IsClopen(\bigcup S.sUnion)$$$

Lean4

theorem isClopen_sUnion (hS : ∀ s ∈ S, IsClopen s) : IsClopen (⋃₀ S) :=
  ⟨isClosed_sUnion fun s hs ↦ (hS s hs).1, isOpen_sUnion fun s hs ↦ (hS s hs).2⟩

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

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

Разделы

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

Аффилиация

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