# Zulip Chat Archive

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