English
A nonempty preorder with no minimal element is infinite, by duality with NoMaxOrder: there exists a strictly increasing sequence in the dual order.
Русский
Не пустой порядок без минимального элемента бесконечен, можно получить через двойственность к NoMaxOrder: существует строго возрастающая последовательность в двойственном порядке.
LaTeX
$$$\exists f: \mathbb{N} \to \alpha\text{ with } \forall n,\ f(n) < f(n+1)$$$
Lean4
/-- A nonempty preorder with no minimal element is infinite. -/
instance infinite [Nonempty α] [NoMinOrder α] : Infinite α :=
@NoMaxOrder.infinite αᵒᵈ _ _ _