toOrderTop

Mathlib.Order.WellFounded

URI: https://scilib.ai/kg/mathlib#WellFoundedGT.toOrderTop

Lean4

/-- A nonempty linear order with well-founded `>` has a top element. -/
noncomputable def toOrderTop {α} [LinearOrder α] [Nonempty α] [WellFoundedGT α] : OrderTop α :=
  have := WellFoundedLT.toOrderBot (α := αᵒᵈ)
  inferInstanceAs (OrderTop αᵒᵈᵒᵈ)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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