closure_is_closed

Mathlib.Order.Closure

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

English

For all x ∈ α, u(l(x)) ∈ l.closed.

Русский

Для любого x ∈ α элемент u(l(x)) принадлежит l.closed.

LaTeX

$$$u(l(x)) \in l.closed$$$

Lean4

@[simp]
theorem closure_is_closed (x : α) : u (l x) ∈ l.closed :=
  l.idempotent x

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

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

Разделы

Аффилиация

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