closure_iUnion — Mathlib

English

For a family of sets s(i), closure of their union equals the supremum of the closures: closure(⋃i s(i)) = ⨆i closure(s(i)).

Русский

Для семейства множеств s(i) замыкание их объединения равно верхней границе замыканий: closure(⋃i s(i)) = ⨆i closure(s(i)).

LaTeX

$$$\mathrm{closure}\left(\bigcup_{i} s(i)\right) = \bigvee_{i} \mathrm{closure}(s(i))$$$

Lean4

theorem closure_iUnion {ι} (s : ι → Set R) : closure (⋃ i, s i) = ⨆ i, closure (s i) :=
  (Subsemiring.gi R).gc.l_iSup

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