How to get the least element of a set of natural numbers?

Stream: new members

[Adam Dingle]

Suppose I have a Set ℕ, i.e. a set of natural numbers. How can I say "Let m be the least element of the set?" Surely Lean knows that the naturals are well-ordered so the least element must exist. I looked around a bit in Mathlib.Init.Set and Mathlib.Order, but I don't see how to proceed.

[Yaël Dillies]

If s : Set ℕ, then you can talk about ⨅₀ s

[Yaël Dillies]

This is docs#sInf

[Bulhwi Cha]

I get "404 Not Found." This will do instead: docs#InfSet.sInf.

[Adam Dingle]

Yaël: Excellent, thanks!

[Ruben Van de Velde]

There's also docs#Nat.find

[Adam Dingle]

Ruben Van de Velde said:

There's also docs#Nat.find

Aha - thanks, good to know.