Greatest elements of finite chains #
A chain need not have a greatest element, and a finite set need not have one either, but a finite chain always does: comparability upgrades a maximal element to a greatest one.
The order is an arbitrary reflexive transitive ≤ rather than a Preorder, matching the level of
Set.Finite.exists_maximal, so the result also applies to a relation carrying no Preorder
instance. Every preorder supplies both instances.
Main results #
IsChain.exists_isGreatest: a nonempty finite chain has a greatest element.
theorem
IsChain.exists_isGreatest
{α : Type u_1}
[LE α]
[IsTrans α fun (x1 x2 : α) => x1 ≤ x2]
[Std.Refl fun (x1 x2 : α) => x1 ≤ x2]
{s : Set α}
(hchain : IsChain (fun (x1 x2 : α) => x1 ≤ x2) s)
(hfin : s.Finite)
(hne : s.Nonempty)
:
∃ (a : α), IsGreatest s a
A nonempty finite chain has a greatest element.