fin find

Stream: general

[Michael Howes]

Suppose that I have a set s : set (fin n) and I know that s is non-empty and that s is a decidable predicate on fin n. Is there a way to produce the least element of s? I was hoping to find something similar to nat.find for fin but haven't come across it yet.

[Scott Morrison]

Convert it to a finset, then use finset.sorted to produce a list, then take the head? I don't know of an existing function.

[Michael Howes]

How do I do the first conversion?

[Johan Commelin]

finset.univ.filter (\lam x, x \in s)??

[Michael Howes]

Thanks!

[Michael Howes]

I ended up using finset.min'