closure_sUnion — Mathlib

English

Closure over a union of sets indexed by a set of sets: closure(⋃₀ s) = ⨆ t ∈ s, closure t.

Русский

Замыкание данного объединения по множества множеств: closure(⋃₀ s) = ⨆ t ∈ s, closure 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 :=
  (NonUnitalSubring.gi R).gc.l_sSup

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