min'_lt_max'_of_card — Mathlib

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

Похожие утверждения