# Re: [isabelle] finite order allows maxima

• To: cl-isabelle-users at lists.cam.ac.uk
• Subject: Re: [isabelle] finite order allows maxima
• From: Stepan Holub <holub at karlin.mff.cuni.cz>
• Date: Tue, 6 Oct 2020 11:53:28 +0200
• References: <mailman.13596.1601974990.3984.cl-isabelle-users@lists.cam.ac.uk>
• User-agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:68.0) Gecko/20100101 Thunderbird/68.12.1

```Dear Tobias,

```
the absence of the simpler lemma is even more surprising. It seems to me moreover that the version for minimum is not easily obtained either.
```
Nevertheless, I understood two things, thank to this mailing list:

```
1. Dmitriy pointed out that any acyclic relation on a finite list is known to be wf, whence both maxima and minima are obtained. Which leads much better proof (posted by Dmitriy up the thread) than the mine is.
```
```
2. Manuel pointed out that arg_max/arg_min can be used. Indeed, for minima we have ex_min_if_finite in Lattices_Big:
```lemma "⟦ finite S; S ≠ {} ⟧ ⟹ ∃m∈S. ¬(∃x∈S. x < (m::'a::order))"
(a side issue: I do not understand why I cannot get alternative
lemma (in order) "⟦ finite S; S ≠ {} ⟧ ⟹ ∃m∈S. ¬(∃x∈S. x < m)"
)
while for maxima a similar claim is missing at the moment.

```
Altogether, it seems to me that a lacking synchronization between "order" "relation" and possibly "Lattices_Big" is somehow at play here. Therefore, I really cannot tell whether adding the lemma is the cleanest solution strategically, although, of course, it would be handy practically.
```
Stepan

On 06-Oct-20 11:03 AM, cl-isabelle-users-request at lists.cam.ac.uk wrote:
```
```On 03/10/2020 10:37, Stepan Holub wrote:
```
```Dear all,

in need (of a particular instance of) the following obvious fact:

lemma (in order) fin_max: "finite A ⟹ a ∈ A ⟹ ∃ s ∈ A. a ≤ s ∧  (∀ b ∈ A. s ≤ b
⟶ s = b)"
```
```This is a useful theorem and I am happy to add it. However, it seems more
modular to prove the simpler

lemma (in order) finite_has_max: "finite A ⟹ A ≠ {} ⟹ ∃ s ∈ A. (∀ b ∈ A. s ≤ b ⟶
s = b)"
```
```

--
Tento e-mail byl zkontrolován na viry programem AVG.
http://www.avg.cz

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.