supClosure_idem

Mathlib.Order.SupClosed

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

English

supClosure is idempotent: applying it twice yields the same set as applying it once.

Русский

supClosure идемпотентно: повторное применение дает тот же набор, что и первое.

LaTeX

$$$\\operatorname{supClosure}(\\operatorname{supClosure}(s)) = \\operatorname{supClosure}(s)$$$

Lean4

theorem supClosure_idem (s : Set α) : supClosure (supClosure s) = supClosure s :=
  supClosure.idempotent _

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

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

Разделы

Аффилиация

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