closure_sUnion — Mathlib

English

For a set s of sets, the closure of their union equals the supremum over all t in s of closure(t).

Русский

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

LaTeX

$$$\mathrm{closure}(\bigcup_{t \in s} t) = \bigvee_{t \in s} \mathrm{closure}(t)$$$

Lean4

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

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