## Stream: Is there code for X?

### Topic: smallest element of a set?

#### Kevin Lacker (Oct 05 2020 at 16:11):

Is there a way to express specifically, "the smallest element of s" where s is a set of natural numbers

#### Kevin Lacker (Oct 05 2020 at 16:20):

so I have to import something for .min to work on set \N, right? how do I figure out what to import

#### Markus Himmel (Oct 05 2020 at 16:21):

I might be wrong, but I don't think you can make it work with dot notation. I think you have to write well_founded.min nat.lt_wf S S_nonempty

#### Johan Commelin (Oct 05 2020 at 16:25):

Kevin Lacker said:

how do I figure out what to import

by asking here... and after a while you'll know the library well enough that you start answering these questions yourself (-;

also grep helps me to find stuff quite often.

#### Kevin Lacker (Oct 05 2020 at 16:31):

ok. why does some stuff work with dot notation and some stuff not work with dot notation?

#### Markus Himmel (Oct 05 2020 at 16:36):

Roughly speaking: if X is of type foo (possibly with some arguments), then dot notation allows us to write X.bar as a shorthand for foo.bar X. So in order to write S.min, where S is a set, the declaration would have to be named set.min

#### Kevin Lacker (Oct 05 2020 at 16:39):

hmm. why isn't a set of natural numbers a well-founded set? i guess because it is only relative to a particular relation

#### Bryan Gin-ge Chen (Oct 05 2020 at 16:40):

For more on dot notation see the end of 3.3.1 and 9.1 in TPiL. I think it finally clicked for me though after I read this thread.

#### Kevin Lacker (Oct 05 2020 at 16:40):

well, i'm used to it in the context of programming languages

#### Kevin Lacker (Oct 05 2020 at 16:40):

the real question in my head is, why isn't .min a function on sets of integers, like it would be in a "normal" programming language

#### Kevin Lacker (Oct 05 2020 at 16:42):

for some reason, i'm sure it's a good one, it doesn't just use the sane default of < for the less-than relation

#### Kevin Lacker (Oct 05 2020 at 16:44):

i read that thread but there's too many references to other concepts i don't get for me to really get it. which is ok... compared to a normal programming language there's just far more methods and far fewer classes, so their organization is kind of necessarily harder to get through

#### Yakov Pechersky (Oct 05 2020 at 16:48):

Do you mean .min a function on finsets of integers?

#### Yakov Pechersky (Oct 05 2020 at 16:49):

Because your_min {x : Z | x < 0} is ...?

#### Kevin Lacker (Oct 05 2020 at 16:49):

sorry, natural numbers, not integers

#### Yakov Pechersky (Oct 05 2020 at 16:50):

Well, I think docs#finset.min' would work for what you want.

#### Johan Commelin (Oct 05 2020 at 16:51):

@Kevin Lacker You can use S.min once you define set.min. But if you define set.min only for S : set nat then mathlib will not like it, because that definition is too restrictive. So you will have to come up with a definition of set.min that is sufficiently general that it covers all cases that one possibly would want to call set.min.

#### Kevin Lacker (Oct 05 2020 at 16:57):

i see. so it kind of tracks back to, there is no way to define a function that sometimes throws an error, or that is only defined on some subset of its input.

#### Yakov Pechersky (Oct 05 2020 at 16:58):

There is, using option or subtype.

#### Yakov Pechersky (Oct 05 2020 at 16:59):

Depends on what you want to do. Compare the docs#finset.min and docs#finset.min'

#### Kevin Lacker (Oct 05 2020 at 17:00):

ok i have to read up more to discuss this sufficiently intelligently

#### Paul van Wamelen (Oct 05 2020 at 18:46):

There is a nice example of getting the smallest nat in a set of nats around line 127 of C:\Projects\lean\mathlib_ufm2\archive\imo\imo1988_q6.lean.

#### Kevin Lacker (Oct 05 2020 at 19:13):

well_founded.not_lt_min nat.lt_wf S S_nonempty hk it is

#### Kevin Lacker (Oct 05 2020 at 22:26):

and after all that, reviewer complains that the simplest way to write this is to use the is_least predicate :rolling_eyes: ( but thank you for pointing that out @Yury G. Kudryashov )

#### Yury G. Kudryashov (Oct 05 2020 at 22:28):

I'm sorry for not telling this earlier. When I read the original question, I thought you were asking about a function that takes a set and returns its minimal element.

#### Yury G. Kudryashov (Oct 05 2020 at 22:28):

Probably we should ask for #xy every time.

#### Kevin Lacker (Oct 05 2020 at 22:29):

sigh... yeah, i should have realized that the answer to these two questions would live in totally different sublibraries

Last updated: May 17 2021 at 16:26 UTC