Zulip Chat Archive

Stream: Is there code for X?

Topic: nonempty linear_order


view this post on Zulip Johan Commelin (Feb 27 2021 at 08:04):

Does mathlib know that every type admits a linear order?

view this post on Zulip Mario Carneiro (Feb 27 2021 at 08:23):

It knows every type admits a well order

view this post on Zulip Mario Carneiro (Feb 27 2021 at 08:32):

import set_theory.ordinal

example (α : Type*) : nonempty (linear_order α) :=
is_well_order.linear_order well_ordering_rel

view this post on Zulip Johan Commelin (Feb 27 2021 at 08:38):

Merci beaucoup!


Last updated: May 17 2021 at 15:13 UTC