closure_iUnion — Mathlib

English

Closure distributes over indexed unions: closure(⋃ i, s i) = ⨆ 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

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

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