Zulip Chat Archive

Stream: new members

Topic: Linear orders


view this post on Zulip Heather Macbeth (Jul 29 2020 at 13:56):

I am trying to navigate the order library. How would I express that something is a linear_order and also has and elements? Do I use [linear_order ι] [bounded_lattice ι]? (I fear that I would be introducing an order twice by doing this.)

view this post on Zulip Johan Commelin (Jul 29 2020 at 13:59):

Yup... that wouldn't work :sad: It would be nice to have mixins here...

view this post on Zulip Johan Commelin (Jul 29 2020 at 13:59):

I guess complete_linear_order gives you more than you want, right?

view this post on Zulip Heather Macbeth (Jul 29 2020 at 14:01):

It's more than necessary. But it's fine for my purposes (closed intervals in the reals, ultimately). Thanks!

view this post on Zulip Adam Topaz (Jul 29 2020 at 14:36):

That's strange... Closed intervals form a linear order? Doesn't linear order require that any two things are comparable?

view this post on Zulip Heather Macbeth (Jul 29 2020 at 14:44):

The order on the points in a single closed interval.

view this post on Zulip Adam Topaz (Jul 29 2020 at 14:46):

Oh :)

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 03:56):

If you're going to add a def for complete_linear_order (Icc a b) it should assume conditionally_complete_linear_order α. It can't be an instance because it also needs a ≤ b`.


Last updated: May 15 2021 at 02:11 UTC