isLUB_iff_sSup_eq

Mathlib.Order.CompleteLattice.Defs

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

English

IsLUB s a if and only if sSup s = a.

Русский

IsLUB s a тогда и только тогда, когда sSup s = a.

LaTeX

$$$ IsLUB\, s\ a \iff sSup\, s = a $$$

Lean4

theorem isLUB_iff_sSup_eq : IsLUB s a ↔ sSup s = a :=
  ⟨(isLUB_sSup s).unique, by rintro rfl; exact isLUB_sSup _⟩

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

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

Разделы

Аффилиация

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