closure_union — Mathlib

English

The closure of the union equals the join of closures: closure(s ∪ t) = closure(s) ⊔ closure(t).

Русский

Замыкание объединения равно объединению замыканий: closure(s ∪ t) = closure(s) ⊔ closure(t).

LaTeX

$$$\\mathrm{closure}(s \\cup t) = \\mathrm{closure}(s) \\sqcup \\mathrm{closure}(t)$$$

Lean4

@[to_additive]
theorem closure_union (s t : Set M) : closure (s ∪ t) = closure s ⊔ closure t :=
  (Subsemigroup.gi M).gc.l_sup

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