closure_iUnion — Mathlib

English

Let K be a division ring and (s_i) a family of subsets of K. The closure of the union equals the supremum of the closures: closure(⋃_i s_i) = ⨆_i closure(s_i).

Русский

Пусть K — деление кольца, и дана семья подмножеств (s_i) ⊆ K. Замыкание объединения равняется наибольшему элементу замкнутых: closure(⋃_i s_i) = ⨆_i closure(s_i).

LaTeX

$$$\operatorname{closure}\left(\bigcup_{i} s_i\right) = \bigvee_{i} \operatorname{closure}(s_i)$$$

Lean4

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

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