smallest element of a set?

Stream: Is there code for X?

[Kevin Lacker]

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

[Markus Himmel]

There are docs#well_founded.min (see also docs#nat.lt_wf) and docs#nat.find.

[Kevin Lacker]

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

[Markus Himmel]

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]

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]

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

[Markus Himmel]

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]

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]

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]

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

[Kevin Lacker]

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]

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]

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]

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

[Yakov Pechersky]

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

[Kevin Lacker]

sorry, natural numbers, not integers

[Yakov Pechersky]

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

[Johan Commelin]

@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]

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]

There is, using option or subtype.

[Yakov Pechersky]

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

[Kevin Lacker]

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

[Paul van Wamelen]

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]

well_founded.not_lt_min nat.lt_wf S S_nonempty hk it is

[Kevin Lacker]

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]

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]

Probably we should ask for #xy every time.

[Kevin Lacker]

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