closure_biUnion — Mathlib

English

Let X be a topological space and s be a Finset of indices with f: ι → Set X. Then closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i).

Русский

Пусть X — топологическое пространство, s — конечный набор индексов Finset, и f: ι → Set X. Тогда closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i).

LaTeX

$$$\\\\overline{\\\\bigcup_{i \\\\in s} f(i)} = \\\\bigcup_{i \\\\in s} \\\\overline{f(i)}$$$

Lean4

@[simp]
theorem closure_biUnion {ι : Type*} (s : Finset ι) (f : ι → Set X) : closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i) :=
  s.finite_toSet.closure_biUnion f

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