isClopen_biUnion — Mathlib

English

If s is finite and h(i) are clopen for all i in s, then the union over i ∈ s of f(i) is clopen.

Русский

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

LaTeX

$$$s.{\finite} \Rightarrow (\forall i \in s, IsClopen(f(i))) \Rightarrow IsClopen(\bigcup_{i \in s} f(i))$$$

Lean4

theorem isClopen_biUnion {Y} {s : Set Y} {f : Y → Set X} (hs : s.Finite) (h : ∀ i ∈ s, IsClopen <| f i) :
    IsClopen (⋃ i ∈ s, f i) :=
  ⟨hs.isClosed_biUnion fun i hi => (h i hi).1, isOpen_biUnion fun i hi => (h i hi).2⟩

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