instOrderTop

Mathlib.Order.Sublocale

URI: https://scilib.ai/kg/mathlib#Sublocale.carrier.instOrderTop

English

The carrier S has a top element; in particular top ∈ S and top is the greatest element of S.

Русский

Носитель S имеет верхний элемент; в частности, ∎ ∈ S и он является наибольшим элементом S.

LaTeX

$$$\top \in S$$$

Lean4

instance instOrderTop : OrderTop S :=
  Subtype.orderTop top_mem

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

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

Разделы

Аффилиация

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