Well-ordering of the integers

Stream: Is there code for X?

[Heather Macbeth]

Does mathlib have the max of a nonempty bounded-above subset of $\mathbb{Z}$?

example (s : set ℤ) (h₁ : nonempty s) (h₂ : bdd_above s) : ∃ k, is_greatest s k

[Yury G. Kudryashov]

docs#int.exists_greatest_of_bdd

[Yury G. Kudryashov]

Found by git grep bdd src/data/int

[Heather Macbeth]

Great, thank you!

[Caleb Schultz Kisby]

I hope it's okay for me to piggyback off of this much older thread.
Is there code for more generic applications of the Well-ordering principle? i.e. if I have my own (finite or lower-bounded) type with a custom ordering on that type, is there existing code that will let me grab the least element?

[Mario Carneiro]

WellFounded.min?

[Siddhartha Gadgil]

A related question: for the minimum of a non-empty set of natural numbers, I found an expression for example:
Nat.lt_wfRel.wf.min {n: ℕ | n % 2 = 0} (by use 2; simp)

Is there something nicer than Nat.lt_wfRel.wf.min to use here?

[Mario Carneiro]

Nat.find

[Siddhartha Gadgil]

Mario Carneiro said:

Nat.find

Thanks a lot. That is computable too.

[Caleb Schultz Kisby]

Thanks @Mario Carneiro, that's what I was looking for! Now I just need to figure out how to use it in my specific case :)

[Caleb Schultz Kisby]

Actually, Nat.find is even better, I just need to change the less-than relation!