closure_union_closure_subset

Mathlib.Order.Closure

URI: https://scilib.ai/kg/mathlib#LowerAdjoint.closure_union_closure_subset

English

For all x,y ∈ α, the union (l x) ∪ (l y) is contained in l(x ∪ y).

Русский

Для любых x,y ∈ α выполнено (l x) ∪ (l y) ⊆ l(x ∪ y).

LaTeX

$$$(l x : Set\beta) \cup l y \subseteq l(x \cup y)$$$

Lean4

theorem closure_union_closure_subset (x y : α) : (l x : Set β) ∪ l y ⊆ l (x ∪ y) :=
  l.closure_sup_closure_le x y

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru