Zulip Chat Archive

Stream: general

Topic: is_well_order


view this post on Zulip Floris van Doorn (Mar 13 2019 at 18:33):

What is the reason that is_well_order is used in the library (for example for ordinals), but that it doesn't extend the other order structures, like linear order? Why is it used in instead of having an argument [well_order α] which extends linear_order?

view this post on Zulip Mario Carneiro (Mar 13 2019 at 18:35):

it's less easy to deal with linear_order objects as if they were just relations

view this post on Zulip Mario Carneiro (Mar 13 2019 at 18:36):

also I had some issues with the fact that the hierarchy was built on le instead of lt

view this post on Zulip Mario Carneiro (Mar 13 2019 at 18:36):

at least, that's what I remember

view this post on Zulip Floris van Doorn (Mar 13 2019 at 18:37):

well, most classes in the hierarchy have both le and lt, right?
If I want to use lemmas about linear_order, is the nicest thing to do just to have a local instance?

view this post on Zulip Mario Carneiro (Mar 13 2019 at 18:56):

yeah, that's what I do in the ordinal proofs

view this post on Zulip Mario Carneiro (Mar 13 2019 at 18:56):

there is a function for that

view this post on Zulip Floris van Doorn (Mar 13 2019 at 18:57):

ok, thanks

view this post on Zulip Mario Carneiro (Mar 13 2019 at 18:58):

linear_order_of_STO'


Last updated: May 11 2021 at 13:22 UTC