idempotent

Mathlib.Order.Closure

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

English

For all x ∈ α, applying closure twice yields the same as once: u(l(u(l(x)))) = u(l(x)).

Русский

При повторном применении замыкания получаем тот же результат: u(l(u(l(x)))) = u(l(x)).

LaTeX

$$$u(l(u(l(x)))) = u(l(x))$$$

Lean4

theorem idempotent (x : α) : u (l (u (l x))) = u (l x) :=
  l.closureOperator.idempotent _

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

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

Разделы

Аффилиация

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