closure_union_closure_right

Mathlib.Order.Closure

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem closure_union_closure_right (x y : α) : l (x ∪ l y) = l (x ∪ y) :=
  SetLike.coe_injective (l.closure_sup_closure_right x y)

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

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

Разделы

Аффилиация

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