# Re: [isabelle] finite order allows maxima

```The names should be “maximal” rather than “max”. The latter would suggest the Max function, which is only meaningful for linear orderings.

Larry

> On 6 Oct 2020, at 08:03, Tobias Nipkow <nipkow at in.tum.de> 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)"
>
> first and derive
>
> lemma (in order) finite_has_max2: "finite A ⟹ a ∈ A ⟹ ∃ s ∈ A. a ≤ s ∧ (∀ b ∈ A. s ≤ b ⟶ s = b)"
>
> from it in one line. In fact, I wonder if the second one is basic enough to go into Main, but probably yes.
>
> I would add the lemma(s) to Finite_Set using Stepan's proof because that way they are added at the earliest point.
>
>
> Tobias
>
>> I have proved it for myself (see below). I wonder whether it can be obtained somehow more directly from Main.
>> Best regards
>> Stepan
>> proof (induct "card {b ∈ A. a < b}" arbitrary: a rule: nat_less_induct)
>>   case 1
>>   have IH: "⋀ x. x ∈ A ⟹ card {b ∈ A. x < b} < card {b ∈ A. a < b} ⟹ ∃s∈A. x ≤ s ∧ (∀b∈A. s ≤ b ⟶ s = b)"
>>     by (simp add: "1.hyps" ‹finite A›)
>>   then show ?case
>>   proof (cases "∀b∈A. a ≤ b ⟶ a = b")
>>     assume "∀b∈A. a ≤ b ⟶ a = b"
>>     thus ?thesis
>>       using ‹a ∈ A› by blast
>>   next
>>     assume "¬ (∀b∈A. a ≤ b ⟶ a = b)"
>>     then obtain a' where "a' ∈ A" and "a < a'"
>>       using local.antisym_conv1 by blast
>>     have "{b ∈ A. a' < b} ⊂ {b ∈ A. a < b}" (is "?Ma' ⊂  ?Ma")
>>     proof-
>>       have "a' ∈ ?Ma" and "a' ∉ ?Ma'" and "⋀ c. c ∈ ?Ma' ⟹ c ∈ ?Ma"
>>         using ‹a < a'› ‹a' ∈ A› by auto
>>       thus "?Ma' ⊂  ?Ma"
>>         by blast
>>     qed
>>     hence card: "card {b ∈ A. a' < b} < card {b ∈ A. a < b}"
>>       by (simp add: ‹finite A› psubset_card_mono)
>>     then obtain s where "s ∈ A" "a' ≤ s ∧ (∀b∈A. s ≤ b ⟶ s = b)"
>>       using IH[OF ‹a' ∈ A› card] by blast
>>     hence "a ≤ s ∧ (∀b∈A. s ≤ b ⟶ s = b)"
>>       using ‹a < a'› by auto
>>     thus ?thesis
>>       using ‹s ∈ A› by blast
>>   qed
>> qed
>

```

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