# 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
*In-reply-to*: <mailman.13596.1601974990.3984.cl-isabelle-users@lists.cam.ac.uk>
*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.*