supClosed_supClosure

Mathlib.Order.SupClosed

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

English

supClosure(s) is closed under finite joins; i.e., it is SupClosed.

Русский

supClosure(s) замкнуто по операциям конечного объединения (join).

LaTeX

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

Lean4

@[simp]
theorem supClosed_supClosure : SupClosed (supClosure s) :=
  supClosure.isClosed_closure _

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

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

Разделы

Аффилиация

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