closure_sUnion — Mathlib

English

Let S be a set of subsets of K. Then the closure of their sUnion equals the supremum of the closures: closure(⋃₀ S) = ⨆_{t ∈ S} closure(t).

Русский

Пусть S — множество подмножеств K. Тогда замыкание их объединения по множеству (sUnion) равно верхней границе замыканий: closure(⋃₀ S) = ⨆_{t ∈ S} closure(t).

LaTeX

$$$\operatorname{closure}(\bigcup S) = \bigvee_{t \in S} \operatorname{closure}(t)$$$

Lean4

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

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