closure_union — Mathlib

English

The closure of the union of two sets equals the supremum of their closures in the Subsemiring lattice.

Русский

Замыкание объединения двух множеств равно верхней границе замыканий этих множеств в решётке подполуколец.

LaTeX

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

Lean4

theorem closure_union (s t : Set R) : closure (s ∪ t) = closure s ⊔ closure t :=
  (Subsemiring.gi R).gc.l_sup

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