closure_sUnion — Mathlib

English

Let α be a topological space which is Alexandrov-discrete. For any collection S of subsets of α, the closure of the union of S equals the union over all s in S of the closure of s.

Русский

Пусть α — топологическое пространство, являющееся Александрово-дискретным. Для любой семействe S подмножеств α выполняется: замыкание объединения всех элементов S равно объединению замыканий каждого элемента.

LaTeX

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

Lean4

theorem closure_sUnion (S : Set (Set α)) : closure (⋃₀ S) = ⋃ s ∈ S, closure s := by
  simp_rw [sUnion_eq_biUnion, closure_iUnion]

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