isLUB_singleton

Mathlib.Order.Bounds.Basic

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

English

The singleton {a} has a as its least upper bound.

Русский

Единственный элемент множества {a} имеет наименьшую верхнюю границу.

LaTeX

$$$ IsLUB\ { a \ }\ a $$$

Lean4

@[simp]
theorem isLUB_singleton : IsLUB { a } a :=
  isGreatest_singleton.isLUB

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

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

Разделы

Аффилиация

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