closure_sUnion — Mathlib

English

For a set of sets S, closure of the union over S equals the supremum over closures of each member of S.

Русский

Для множества множеств S, замыкание объединения по S равно наибольшему замыканию каждого элемента.

LaTeX

$$$\\mathrm{closure}(\\bigcup\\mathcal{S}) = \\bigsqcup_{t\\in \\mathcal{S}} \\mathrm{closure}(t)$$$

Lean4

theorem closure_sUnion (s : Set (Set R)) : closure (⋃₀ s) = ⨆ t ∈ s, closure t :=
  (Subring.gi R).gc.l_sSup

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