latticeClosure_idem

Mathlib.Order.SupClosed

URI: https://scilib.ai/kg/mathlib#latticeClosure_idem

English

latticeClosure is idempotent: latticeClosure(latticeClosure(s)) = latticeClosure(s).

Русский

Замыкание по решётке идемпотентно: latticeClosure(latticeClosure(s)) = latticeClosure(s).

LaTeX

$$$\mathrm{latticeClosure}(\mathrm{latticeClosure}(s)) = \mathrm{latticeClosure}(s)$$$

Lean4

theorem latticeClosure_idem (s : Set α) : latticeClosure (latticeClosure s) = latticeClosure s :=
  latticeClosure.idempotent _

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

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

Разделы

Аффилиация

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