bddAbove_singleton

Mathlib.Order.Bounds.Basic

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

English

The singleton {a} is bounded above.

Русский

Множество {a} ограничено сверху.

LaTeX

$$$ BddAbove\ ({ a } : Set α) $$$

Lean4

@[simp]
theorem bddAbove_singleton : BddAbove ({ a } : Set α) :=
  isLUB_singleton.bddAbove

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

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

Разделы

Аффилиация

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