sSup_singleton

Mathlib.Order.CompleteLattice.Basic

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

English

The supremum of a singleton set {a} is a itself.

Русский

Наименьшее верхнее для множества из одного элемента равно этому элементу.

LaTeX

$$$$ \operatorname{sSup} \{a\} = a $$$$

Lean4

@[simp]
theorem sSup_singleton {a : α} : sSup { a } = a :=
  isLUB_singleton.sSup_eq

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

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

Разделы

Аффилиация

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