## Stream: Is there code for X?

### Topic: non-dense orders

#### 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

#### 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

#### Mario Carneiro (Oct 21 2020 at 12:07):

no that doesn't exist AFAIK

#### Johan Commelin (Oct 21 2020 at 12:08):

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

#### Mario Carneiro (Oct 21 2020 at 12:09):

it sounds sort of like sigma finite for counting measure

#### Mario Carneiro (Oct 21 2020 at 12:11):

or maybe locally finite

#### 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.

#### Mario Carneiro (Oct 21 2020 at 12:11):

bounded sets are finite

#### 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'.

#### Johan Commelin (Oct 21 2020 at 12:12):

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

#### Mario Carneiro (Oct 21 2020 at 12:13):

Yeah, the intervals were designed with that use in mind

#### 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

#### 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