closure_union_closure

Mathlib.Order.Closure

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

English

For all x,y ∈ α, l(l x ∪ l y) = l(x ∪ y).

Русский

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

LaTeX

$$$l(l(x) \cup l(y)) = l(x \cup y)$$$

Lean4

theorem closure_union_closure (x y : α) : l (l x ∪ l y) = l (x ∪ y) := by
  rw [closure_union_closure_right, closure_union_closure_left]

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

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

Разделы

Аффилиация

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