upperClosure_union — Mathlib

English

The upper closure of a union equals the infimum of the corresponding upper closures: upperClosure(s ∪ t) = upperClosure(s) ⊓ upperClosure(t).

Русский

Верхнее замыкание объединения равно наименьшему верхнему объединению: верхнее замыкание (s ∪ t) = верхнее замыкание s ∧ верхнее замыкание t.

LaTeX

$$$\mathrm{upperClosure}(s \cup t) = \mathrm{upperClosure}(s) \;\sqcap\; \mathrm{upperClosure}(t)$$$

Lean4

@[simp]
theorem upperClosure_union (s t : Set α) : upperClosure (s ∪ t) = upperClosure s ⊓ upperClosure t :=
  (@gc_upperClosure_coe α _).l_sup

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