isClopen_iUnion₂

Mathlib.Topology.AlexandrovDiscrete

URI: https://scilib.ai/kg/mathlib#isClopen_iUnion₂

← MathLib Explorer

English

If every f(i,j) is clopen, then the union over i and j is clopen.

Русский

Если каждое f(i,j) — clopen, то объединение по i и j — clopen.

LaTeX

$$$\forall i,\forall j, IsClopen(f(i,j)) \Rightarrow IsClopen(\bigcup_i\bigcup_j f(i,j))$$$

Lean4

theorem isClopen_iUnion₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsClopen (f i j)) : IsClopen (⋃ i, ⋃ j, f i j) :=
  isClopen_iUnion fun _ ↦ isClopen_iUnion <| hf _

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

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

Разделы

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

Аффилиация

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