isClopen_iInter — Mathlib

English

If f(i) are clopen for all i, then their intersection is clopen.

Русский

Если множества f(i) являются одновременно открытыми и замкнутыми для всех i, то их пересечение также является clopen.

LaTeX

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

Lean4

theorem isClopen_iInter (hf : ∀ i, IsClopen (f i)) : IsClopen (⋂ i, f i) :=
  ⟨isClosed_iInter fun i ↦ (hf i).1, isOpen_iInter fun i ↦ (hf i).2⟩

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