Finite chain has a maximal element

Stream: Is there code for X?

[Eduardo Freire]

Hello, is there code showing that finite chains have maximal elements? I'm thinking about making a PR to mathlib adding Tukey's lemma and it needs this result, but my current proof of it is quite ugly.

Here is the lemma:

import order.chain
import data.set

lemma max_of_fin_chain {α : Type*} [partial_order α] :
∀ {c : set α}, c.finite → is_chain (≤) c → c.nonempty → ∃m ∈ c, ∀ {b}, b ∈ c → b ≤ m := sorry

[Yaël Dillies]

Do you know about docs#finset.exists_min_image, docs#finset.exists_minimal?

[Yaël Dillies]

Isn't Tukey's lemma a direct special case of Hausdorff's maximality principle?

[Eduardo Freire]

Yaël Dillies said:

Do you know about docs#finset.exists_min_image, docs#finset.exists_minimal?

I didn't, was looking for this thanks

[Yaël Dillies]

We're missing a few variants that I was adding the other day. Opening the PR soon.

[Eduardo Freire]

Yaël Dillies said:

Isn't Tukey's lemma a direct special case of Hausdorff's maximality principle?

I used zorn_subset_nonempty instead, not sure if it is more or less direct though :thinking: