closure_insert — Mathlib

English

The closure of s with an added element m equals the join of the closures of {m} and s.

Русский

Замыкание множества s после добавления элемента m равно объединению замыканий {m} и s.

LaTeX

$$$$ \operatorname{closure}_L(\operatorname{insert}(m, s)) = \operatorname{closure}_L(\{m\}) \sqcup \operatorname{closure}_L(s). $$$$

Lean4

theorem closure_insert (s : Set M) (m : M) : closure L (insert m s) = closure L { m } ⊔ closure L s :=
  closure_union { m } s

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