infClosed

Mathlib.Order.SupClosed

URI: https://scilib.ai/kg/mathlib#IsLowerSet.infClosed

English

If s is inf-closed and a is in lowerBounds s, then insert a into s is inf-closed.

Русский

Если s инф-замкнуто и a ∈ lowerBounds s, то вставка a в s сохраняет инф-замкнутость.

LaTeX

$$$ (\\text{InfClosed } s) \\rightarrow (a \\in \\text{lowerBounds } s) \\rightarrow \\text{InfClosed}(\\operatorname{insert} a s) $$$

Lean4

theorem infClosed (hs : IsLowerSet s) : InfClosed s := fun _a _ _b ↦ hs inf_le_right

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

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

Разделы

Аффилиация

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