isClosed_biUnion_finset — Mathlib

English

If s is a finite index set 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_finset {s : Finset α} {f : α → Set X} (h : ∀ i ∈ s, IsClosed (f i)) :
    IsClosed (⋃ i ∈ s, f i) :=
  s.finite_toSet.isClosed_biUnion h

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