Zulip Chat Archive

Stream: Is there code for X?

Topic: non-dense orders


view this post on Zulip Eric Wieser (Oct 21 2020 at 11:50):

Is there a typeclass that applies to nat, int, and fin n which provides the finite ordered list of elements in a range [a, b]? So the opposite of docs#densely_ordered in a way.

I'd like it to revive parts of #3770, but implement swap_eq_prod_swap_adj without specifying just fin n

view this post on Zulip Eric Wieser (Oct 21 2020 at 11:52):

I think a has_succ typeclass would be pretty much all I need, combined with some decidable instance and linear_order

view this post on Zulip Mario Carneiro (Oct 21 2020 at 12:07):

no that doesn't exist AFAIK

view this post on Zulip Johan Commelin (Oct 21 2020 at 12:08):

Do you need succ? Or would a finite_Ico (interval_finite?) class also work?

view this post on Zulip Mario Carneiro (Oct 21 2020 at 12:09):

it sounds sort of like sigma finite for counting measure

view this post on Zulip Mario Carneiro (Oct 21 2020 at 12:11):

or maybe locally finite

view this post on Zulip Johan Commelin (Oct 21 2020 at 12:11):

I can imagine that we might want this for non-linear orders as well, at some point.

view this post on Zulip Mario Carneiro (Oct 21 2020 at 12:11):

bounded sets are finite

view this post on Zulip Johan Commelin (Oct 21 2020 at 12:12):

E.g., I might be interested in the finset of all subgroup of a finite Galois group that contain H and are contained in H'.

view this post on Zulip Johan Commelin (Oct 21 2020 at 12:12):

I wouldn't be opposed to abusing finset.Icc for that.

view this post on Zulip Mario Carneiro (Oct 21 2020 at 12:13):

Yeah, the intervals were designed with that use in mind

view this post on Zulip Mario Carneiro (Oct 21 2020 at 12:14):

although it is much more likely to find posets where all chains are finite but there are infinite intervals

view this post on Zulip Mario Carneiro (Oct 21 2020 at 12:15):

so asserting that intervals are finite bounds both the width and height of the poset


Last updated: May 16 2021 at 05:21 UTC