Is there any function like min::"int set => int" to get the minimal element in one int set

It's called `Min`

, but it only works for finite sets. There's also `Inf`

, the infimum, which also works on infinite sets as long as they are bounded from below.

Manuel Eberl said:

It's called

`Min`

, but it only works for finite sets. There's also`Inf`

, the infimum, which also works on infinite sets as long as they are bounded from below.

thanks. that is what I want

Hello, does there also exist a function of type "('a => 'a => bool) => 'a set => 'a"? I need both the order ('a => 'a => bool) and the (finite) set ('a set) to be variable...

According to

```
find_theorems "_ :: ('a => 'a => bool) => 'a set => 'a"
```

there is `linorder.Min`

but I am not sure how easy it is to use

If there is a unique minimum, you can indeed use that, yes.

And if your relation is indeed a linear ordering on the *entire* type.

Which may be too strong a requirement, alas…

Otherwise you can use something I made: Link to AFP entry

```
definition Max_wrt_among :: "'a relation ⇒ 'a set ⇒ 'a set" where
"Max_wrt_among R A = {x∈A. R x x ∧ (∀y∈A. R x y ⟶ R y x)}"
```

Here, `'a relation`

is just a type synonym for `'a ⇒ 'a ⇒ bool`

.

It should be easy to adapt this to minimum (e.g. by applying it to the dual relation).

Note that this returns a *set*, not a single element. You'd then have to define a version for linear orderings that just returns a single element (`Max_wrt_among`

or `Min_wrt_among`

will then always be singleton sets, so you can use e.g. `the_elem`

to get that element)

wow thanks I will try out! (yes in general it's only an order on the provided set)

Last updated: Sep 25 2022 at 22:23 UTC