non-dense orders

Stream: Is there code for X?

[Eric Wieser]

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]

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

[Mario Carneiro]

no that doesn't exist AFAIK

[Johan Commelin]

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

[Mario Carneiro]

it sounds sort of like sigma finite for counting measure

[Mario Carneiro]

or maybe locally finite

[Johan Commelin]

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

[Mario Carneiro]

bounded sets are finite

[Johan Commelin]

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]

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

[Mario Carneiro]

Yeah, the intervals were designed with that use in mind

[Mario Carneiro]

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

[Mario Carneiro]

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