closure_iUnion — Mathlib

English

Closure distributes over directed unions: closure of ⋃ i s(i) equals ⨆ i closure(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

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

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