Zulip Chat Archive

Stream: general

Topic: is_well_order

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?

Mario Carneiro (Mar 13 2019 at 18:35):

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

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

Mario Carneiro (Mar 13 2019 at 18:36):

at least, that's what I remember

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?

Mario Carneiro (Mar 13 2019 at 18:56):

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

Mario Carneiro (Mar 13 2019 at 18:56):

there is a function for that

Floris van Doorn (Mar 13 2019 at 18:57):

ok, thanks

Mario Carneiro (Mar 13 2019 at 18:58):

linear_order_of_STO'

Last updated: Dec 20 2023 at 11:08 UTC