isClopen_iInter₂

Mathlib.Topology.AlexandrovDiscrete

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

← MathLib Explorer

English

If every f(i,j) is clopen, then the double intersection is clopen.

Русский

Если все f(i,j) являются clopen, то их двойное пересечение clopen.

LaTeX

$$$\forall i,\forall j, IsClopen(f(i,j)) \Rightarrow IsClopen(\bigcap_i\bigcap_j f(i,j))$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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