isLUB_supClosure

Mathlib.Order.SupClosed

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

English

a is a least upper bound of supClosure(s) if and only if a is a least upper bound of s.

Русский

a — наименьшая верхняя грань supClosure(s) тогда и только тогда, когда она является наименьшей верхней гранью s.

LaTeX

$$$\\IsLUB(\\operatorname{supClosure}(s), a) \\iff \\IsLUB(s, a)$$$

Lean4

@[simp]
theorem isLUB_supClosure : IsLUB (supClosure s) a ↔ IsLUB s a := by simp [IsLUB]

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

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

Разделы

Аффилиация

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