closure_union — Mathlib

English

Let s and t be subsets of a monoid M. The submonoid generated by their union equals the join (supremum) of the submonoids generated by each set: closure(s ∪ t) = closure(s) ⊔ closure(t).

Русский

Пусть s и t — подмножества моноида M. Замыкание по объединению s ∪ t равно объединению (верхней границе) замыканий по s и по t: closure(s ∪ t) = closure(s) ⊔ closure(t).

LaTeX

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

Lean4

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

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