closure_sUnion — Mathlib

English

Let X be a topological space and S be a finite set of subsets of X. Then closure (⋃₀ S) = ⋃ s ∈ S, closure s.

Русский

Пусть X — топологическое пространство, S — конечное множество подмножеств X. Тогда closure(⋃₀ S) = ⋃ s ∈ S, closure s.

LaTeX

$$$\\\\overline{\\\\bigcup_{s \\\\in S} s} = \\\\bigcup_{s \\\\in S} \\\\overline{s}$$$

Lean4

theorem closure_sUnion {S : Set (Set X)} (hS : S.Finite) : closure (⋃₀ S) = ⋃ s ∈ S, closure s := by
  rw [sUnion_eq_biUnion, hS.closure_biUnion]

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