@[implicit_reducible]

noncomputable def Coxeter.orderTop_ofFiniteDirectedOrder {α : Type u_1} [Nonempty α] [Preorder α] [Finite α] [IsDirectedOrder α] : OrderTop α

Equations

• Coxeter.orderTop_ofFiniteDirectedOrder = { top := ⋯.choose, le_top := ⋯ }