Canonical way to get minimum element of set of naturals

Stream: new members

[Julian Gilbey]

I have a property defined for natural numbers: p : N -> Prop and I have a subtype { x : N // p x }. I can produce a natural n : N with p n, so this set/subtype is non-empty. Since N is well-ordered, this non-empty subtype/set has a minimum element. But I cannot figure out what Lean incantation I should use to find/refer to this minimum element of this set/subtype.

Any suggestions would be much welcomed, thanks!

[Kevin Buzzard]

You want nat.find -- right click on it and look at the functions defined just after it to see the API available to you

[Julian Gilbey]

Thanks @Kevin Buzzard !

[Julian Gilbey]

Oh, groan, I thought I was getting the hang of this. But now I realise I don't know how to define a lambda expression inside a begin/end argument. I've written:

  have p := λ k : ℕ, x < (k : ℝ) * (1 / (n : ℝ)),

but then the goals just list: p : N -> Prop, and when I get a target of p n0 and I have a term h of exactly the right form (namely, x < (n0 : R) * (1 / (n : R))), Lean refuses to match the two when I say exact h. I guess I should be using something other than have, but I don't know what.

My second problem, once I've resolved this, is that because my predicate uses the reals, I'm guessing it's not decidable. So nat.find presumably won't work. Is there a non-decidable version of nat.find which just asserts the existence of such an element but without attempting to compute it?

[Reid Barton]

Use let not have

[Julian Gilbey]

Ah, magic, thanks! :grinning:

[Reid Barton]

For the second question you could use tactic#classical, or open_locale classical at the top level of your file if this is something you will generally need

[Floris van Doorn]

You can also use Inf {n | p n}, and use the instance docs#nat.conditionally_complete_linear_order_bot and the API about docs#conditionally_complete_linear_order. This does not require the predicate to be decidable.

[Floris van Doorn]

plus some lemmas specific to nat, like docs#nat.Inf_mem

[Yury G. Kudryashov]

Inf doesn't require decidable and is not computable.