Re: [isabelle] finite order allows maxima



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.