not_isMin_succ — Mathlib

English

In a nontrivial linear order, the successor of any element is not the minimum element.

Русский

В ненулевом линейном порядке переход к следующему элементу не является минимальным элементом.

LaTeX

$$$[\text{Nontrivial } \alpha] \Rightarrow \neg\operatorname{IsMin}(\operatorname{succ} a)$$$

Lean4

theorem not_isMin_succ [Nontrivial α] (a : α) : ¬IsMin (succ a) :=
  by
  obtain ha | ha := (le_succ a).eq_or_lt
  · exact (ha ▸ succ_eq_iff_isMax.1 ha.symm).not_isMin
  · exact not_isMin_of_lt ha

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