lowerClosure_union — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem lowerClosure_union (s t : Set α) : lowerClosure (s ∪ t) = lowerClosure s ⊔ lowerClosure t :=
  (@gc_lowerClosure_coe α _).l_sup

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