closure_union_closure_left

Mathlib.Order.Closure

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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