closure_sup_closure_le

Mathlib.Order.Closure

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

English

For all x,y ∈ α, u(l(x)) ⊔ u(l(y)) ≤ u(l(x ⊔ y)).

Русский

Для любых x,y ∈ α, u(l(x)) ⊔ u(l(y)) ≤ u(l(x ⊔ y)).

LaTeX

$$$u(l(x)) \uplus u(l(y)) \\le u(l(x \or y))$$$

Lean4

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

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

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

Разделы

Аффилиация

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