Least extended natural with witness

Stream: Is there code for X?

[bottine]

Hey! Say I have a function D -> nat and I want to find the least n:nat in the range of the function, plus a preimage, or top. Is there something built-in for hat? Ideally D could be a subset instead of a type too.

Also, I'm a bit confused about function.argminfunction on well-orders, how does it deal with empty domains?

[Patrick Massot]

docs#nat.find will help

[bottine]

mmh, thanks

[Vincent Beffara]

Or like this? https://github.com/vbeffara/lean/blob/main/src/graph_theory/metric.lean (well_founded.min_mem)

[bottine]

will, have a look, thanks!