infClosed_infClosure

Mathlib.Order.SupClosed

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

English

InfClosure s is InfClosed; i.e., the closure under infima is closed under infima.

Русский

InfClosure(s) является InfClosed; замыкание по Inf замкнуто по инфимам.

LaTeX

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

Lean4

@[simp]
theorem infClosed_infClosure : InfClosed (infClosure s) :=
  infClosure.isClosed_closure _

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

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

Разделы

Аффилиация

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