@[implicit_reducible]

noncomputable instance Coxeter.instOrderTop_coxeter (α : Type u_1) [Nonempty α] [Preorder α] [Finite α] [IsDirectedOrder α] : OrderTop α

Equations

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