top_mem_upperBounds

Mathlib.Order.Bounds.Basic

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

English

If α has a top element, then ⊤ is an upper bound for any set s.

Русский

Пусть в α есть верхняя граница; тогда ⊤ является верхней границей для любого множества s.

LaTeX

$$$\\top \\in \\text{upperBounds}(s)$$$

Lean4

theorem top_mem_upperBounds [OrderTop α] (s : Set α) : ⊤ ∈ upperBounds s := fun _ _ => le_top

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

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

Разделы

Аффилиация

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