Find the nth element of an ordered finset

Stream: Is there code for X?

[Jujian Zhang]

Given a well order type $\iota$ and a finite set $\sigma$, is there an easy way to find the $n$-th largest element? I.e., what be the easiest way of doing the following:

import data.finset

section examples

variables {ι : Type*} [linear_order ι] [is_well_order ι ((≤) : ι → ι → Prop)]

example (σ : finset ι) : ∃ f : fin σ.card → σ, strict_mono f := sorry

end examples

Thanks for any help

[Yaël Dillies]

Why would you need a well order for this?

[Yaël Dillies]

You can use docs#finset.sort and docs#list.nth

[Eric Wieser]

docs#finset.sort?

[Eric Wieser]

Arguably we should implement a partitioning algorithm which would be faster, but that probably doesn't matter until lean 4

[Jujian Zhang]

Yaël Dillies said:

Why would you need a well order for this?

I don't need well order for this, it just happens that I need to work with well ordered type