# Zulip Chat Archive

## Stream: new members

### Topic: Canonical way to get minimum element of set of naturals

#### Julian Gilbey (Nov 03 2021 at 09:10):

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 (Nov 03 2021 at 09:13):

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 (Nov 03 2021 at 09:13):

Thanks @Kevin Buzzard !

#### Julian Gilbey (Nov 03 2021 at 11:55):

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 (Nov 03 2021 at 11:59):

Use `let`

not `have`

#### Julian Gilbey (Nov 03 2021 at 12:01):

Ah, magic, thanks! :grinning:

#### Reid Barton (Nov 03 2021 at 12:05):

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 (Nov 03 2021 at 13:56):

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 (Nov 03 2021 at 13:57):

plus some lemmas specific to `nat`

, like docs#nat.Inf_mem

#### Yury G. Kudryashov (Nov 04 2021 at 06:25):

`Inf`

doesn't require `decidable`

and is not computable.

Last updated: Dec 20 2023 at 11:08 UTC