isClopen_biInter — Mathlib

English

If s is a finite set of indices and each f(i) is clopen, then the intersection over i in s of f(i) is clopen.

Русский

Если s — конечное множество индексов и для каждого i ∈ s множество f(i) является открытым и замкнутым, то пересечение по i ∈ s множества f(i) является открытым и замкнутым.

LaTeX

$$$ (\\forall i \\in s, IsClopen(f(i))) \\Rightarrow IsClopen\\left(\\bigcap_{i \\in s} f(i)\\right) $$$

Lean4

theorem isClopen_biInter {Y} {s : Set Y} (hs : s.Finite) {f : Y → Set X} (h : ∀ i ∈ s, IsClopen (f i)) :
    IsClopen (⋂ i ∈ s, f i) :=
  ⟨isClosed_biInter fun i hi => (h i hi).1, hs.isOpen_biInter fun i hi => (h i hi).2⟩

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