English
If S is a finite nonempty subset of a linearly ordered set and S contains at least two elements, then the minimum of S is strictly less than the maximum of S.
Русский
Если S — конечное непустое подмножество линейно упорядоченного множества и содержит хотя бы два элемента, то минимум S строго меньше максимумa S.
LaTeX
$$$\\text{Let } \\alpha \\text{ be a linear order and } S \\subseteq \\alpha \\text{ finite nonempty with } |S| \\ge 2. \\text{ Then } \\min S < \\max S.$$$
Lean4
theorem min'_lt_max' {i j} (H1 : i ∈ s) (H2 : j ∈ s) (H3 : i ≠ j) : s.min' ⟨i, H1⟩ < s.max' ⟨i, H1⟩ :=
isGLB_lt_isLUB_of_ne (s.isLeast_min' _).isGLB (s.isGreatest_max' _).isLUB H1 H2 H3
