closure_iUnion — Mathlib

English

Let (s_i) be a family of subsets of M. Then closure of their union equals the supremum of the closures: closure(⋃i s_i) = ⨆ i, closure(s_i).

Русский

Пусть (s_i) — семейство подмножеств M. Тогда замыкание объединения по индексу равно верхнейեմо обобщению замыканий: closure(⋃i s_i) = ⨆i closure(s_i).

LaTeX

$$$\\operatorname{closure}\\Big( \\bigcup_i s_i \\Big) = \\bigvee_i \\operatorname{closure}(s_i)$$$

Lean4

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

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