closure_iUnion — Mathlib

English

Closure distributes over unions: closure of the union equals the union of closures.

Русский

Замыкание распределяется по объединениям: closure(⋃ f_i) = ⋃ closure(f_i).

LaTeX

$$$\operatorname{closure}(\bigcup_i f_i) = \bigcup_i \operatorname{closure}(f_i)$$$

Lean4

theorem closure_iUnion (f : ι → Set α) : closure (⋃ i, f i) = ⋃ i, closure (f i) :=
  compl_injective <| by simpa only [← interior_compl, compl_iUnion] using interior_iInter fun i ↦ (f i)ᶜ

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