# Re: [isabelle] finite order allows maxima

Maybe Min/Max (on finite sets) could be defined for arbitrary orders instead of just linear orders as currently? Florian?
```
Tobias

On 04/10/2020 14:31, Dmitriy Traytel wrote:
```
```Hi Stepan,

an alternative is to use the well-foundedness of > restricted to the finite set A. This gives one maximal elements via wf_eq_minimal. Not sure if this qualifies as “more direct”, but at least no explicit induction is needed.

Dmitriy

lemma (in order) fin_max:
assumes "finite A" "a ∈ A"
shows "∃s ∈ A. a ≤ s ∧ (∀b ∈ A. s ≤ b ⟶ s = b)"
proof -
from ‹finite A› have "wf {(x,y). x ∈ A ∧ y ∈ A ∧ x > y}"
by (intro finite_acyclic_wf[OF finite_subset[of _ "A × A"]]) (auto intro!: acyclicI_order)
with ‹a ∈ A› show ?thesis
unfolding wf_eq_minimal using order.trans order.order_iff_strict
by (elim allE[of _ "{x ∈ A. a ≤ x}"] allE[of _ a]) (auto 7 0)
qed

```
```On 3 Oct 2020, at 10:37, Stepan Holub <holub at karlin.mff.cuni.cz> 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)"

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

--
Tento e-mail byl zkontrolován na viry programem AVG.

```
```
```
```
```

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

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