isClosed_biUnion — Mathlib

English

If s is a finite set of indices and f(i) is closed for all i ∈ s, then ⋃ i ∈ s f(i) is closed.

Русский

Если S — конечное множество индексов и для каждого i ∈ S множество f(i) замкнуто, то объединение ⋃_{i ∈ S} f(i) замкнуто.

LaTeX

$$$(\forall i \in s, \operatorname{IsClosed}(f(i))) \Rightarrow \operatorname{IsClosed}( \bigcup_{i \in s} f(i) )$$$

Lean4

theorem isClosed_biUnion {s : Set α} {f : α → Set X} (hs : s.Finite) (h : ∀ i ∈ s, IsClosed (f i)) :
    IsClosed (⋃ i ∈ s, f i) := by
  simp only [← isOpen_compl_iff, compl_iUnion] at *
  exact hs.isOpen_biInter h

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