← Mathematical handbook

@[instance_reducible]

instance instOrdSubtype {α : Type u} [Ord α] {P : α → Prop} : Ord (Subtype P)

Equations

• instOrdSubtype = { compare := fun (a b : Subtype P) => compare a.val b.val }