isClopen_sInter — Mathlib

English

The intersection of a family of clopen sets is clopen in Alexandrov discrete spaces.

Русский

Пересечение семейства открыто и закрыто (clopen) множеств в пространстве Александрова-дискретного типа.

LaTeX

$$$\forall S:\text{Set}(\text{Set}(\alpha)), (\forall s\in S, \ IsClopen(s)) \Rightarrow IsClopen(S.sInter)$$$

Lean4

theorem isClopen_sInter (hS : ∀ s ∈ S, IsClopen s) : IsClopen (⋂₀ S) :=
  ⟨isClosed_sInter fun s hs ↦ (hS s hs).1, isOpen_sInter fun s hs ↦ (hS s hs).2⟩

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