## Stream: Beginner Questions

### Topic: minimal

#### zibo yang (Jun 02 2021 at 13:17):

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

#### Manuel Eberl (Jun 02 2021 at 13:19):

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.

#### zibo yang (Jun 02 2021 at 14:02):

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

#### Taro Yoshioka (Jul 18 2022 at 14:38):

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...

#### Mathias Fleury (Jul 18 2022 at 14:46):

According to

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

#### Mathias Fleury (Jul 18 2022 at 14:46):

there is `linorder.Min`

#### Mathias Fleury (Jul 18 2022 at 14:47):

but I am not sure how easy it is to use

#### Manuel Eberl (Jul 18 2022 at 14:52):

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

#### Manuel Eberl (Jul 18 2022 at 14:53):

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

#### Manuel Eberl (Jul 18 2022 at 14:53):

Which may be too strong a requirement, alas…

#### Manuel Eberl (Jul 18 2022 at 14:55):

``````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)

#### Taro Yoshioka (Jul 18 2022 at 15:11):

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

Last updated: Aug 13 2022 at 06:26 UTC