closure_sup_closure_left

Mathlib.Order.Closure

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

English

u(l(x ⊔ u(l y))) = u(l(x ⊔ y)).

Русский

u(l(x ⊔ u(l(y)))) = u(l(x ⊔ y)).

LaTeX

$$$u(l(x \\lor u(l(y)))) = u(l(x \\lor y))$$$

Lean4

theorem closure_sup_closure_left (x y : α) : u (l (u (l x) ⊔ y)) = u (l (x ⊔ y)) :=
  l.closureOperator.closure_sup_closure_left x y

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

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

Разделы

Аффилиация

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