Last minimizers on finite sets

A function on a nonempty finite linearly ordered set has a last minimizer: its value is minimal on the set and strictly smaller than its value at every later point of the set.

This is the choice of the last vertex of minimal height in the two-cut construction of Littelmann root operators, used in TauCeti.exists_strictly_rising_of_isAChain.

theorem Finset.exists_last_min_image {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (s : Finset α) (f : α → β) (hs : s.Nonempty) : ∃ a ∈ s, (∀ b ∈ s, f a ≤ f b) ∧ ∀ b ∈ s, a < b → f a < f b

A function on a nonempty finite linearly ordered set attains its minimum at a last point. Every later point of the set has strictly larger value.