closure_iUnion_of_finite — Mathlib

English

Let X be a topological space and f : ι → Set X with ι finite. Then closure (⋃ i, f i) = ⋃ i, closure (f i).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem closure_iUnion_of_finite [Finite ι] (f : ι → Set X) : closure (⋃ i, f i) = ⋃ i, closure (f i) := by
  rw [← sUnion_range, (finite_range _).closure_sUnion, biUnion_range]

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