Re: [isabelle] finite order allows maxima

I have now added some lemmas with succinct proofs (avoiding cardinalities) and followed Manuel's suggestions concerning arg_min.
```See here: http://isabelle.in.tum.de/repos/isabelle/rev/b037517c815b

Tobias

On 06/10/2020 11:53, Stepan Holub wrote:
```
```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)"
```
```

```
```
```

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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