infClosure_idem

Mathlib.Order.SupClosed

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

English

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

Русский

infClosure идемпотентно: infClosure(infClosure(s)) = infClosure(s).

LaTeX

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

Lean4

theorem infClosure_idem (s : Set α) : infClosure (infClosure s) = infClosure s :=
  infClosure.idempotent _

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

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

Разделы

Аффилиация

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