closure_sUnion — Mathlib

English

Closure distributes over sUnion (union of a set of subsets): closure(⋃ t∈s t) = ⨆ t∈s, closure(t).

Русский

Замыкание распространяется на sUnion: closure(⋃ t∈s t) = ⨆ t∈s, closure(t).

LaTeX

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

Lean4

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

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