closure_iUnion — Mathlib

English

The closure of the union of a family of sets equals the join (sup) of the closures of the sets in the family.

Русский

Замыкание объединения семейства множеств равно объединению замыканий этих множеств.

LaTeX

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

Lean4

@[to_additive]
theorem closure_iUnion {ι} (s : ι → Set M) : closure (⋃ i, s i) = ⨆ i, closure (s i) :=
  (Subsemigroup.gi M).gc.l_iSup

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