isClopen_biInter_finset — Mathlib

English

Let X be a topological space and {f(i)} for i in a finite index set s be sets in X such that each f(i) is clopen. Then their intersection over i ∈ s is also clopen.

Русский

Пусть X — топологическое пространство и для конечного множества индексов s имеется семейство множеств f(i) ⊆ X, каждое из которыхclopen. Тогда пересечение ⋂ i ∈ s f(i) также является открытым и замкнутым

LaTeX

$$$$ \operatorname{IsClopen}\left(\bigcap_{i \in s} f(i)\right) $$$$

Lean4

theorem isClopen_biInter_finset {Y} {s : Finset Y} {f : Y → Set X} (h : ∀ i ∈ s, IsClopen (f i)) :
    IsClopen (⋂ i ∈ s, f i) :=
  s.finite_toSet.isClopen_biInter h

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