English
If S is a finite nonempty subset with cardinality greater than 1, then min S < max S.
Русский
Если множество S конечно и непусто иcard(S) > 1, то min S < max S.
LaTeX
$$$S \\subseteq \\alpha \\text{ finite } S \\neq \\varnothing, \\text{ and } |S| > 1 \\Rightarrow \\min S < \\max S.$$$
Lean4
/-- If there's more than 1 element, the min' is less than the max'. An alternate version of
`min'_lt_max'` which is sometimes more convenient.
-/
theorem min'_lt_max'_of_card (h₂ : 1 < card s) :
s.min' (Finset.card_pos.1 <| by cutsat) < s.max' (Finset.card_pos.1 <| by cutsat) :=
by
rcases one_lt_card.1 h₂ with ⟨a, ha, b, hb, hab⟩
exact s.min'_lt_max' ha hb hab