English
A nonempty preorder with no maximal element is infinite: there exists a strictly increasing sequence in α, i.e., an injection f: Nat → α or a strictly increasing function from the natural numbers into α.
Русский
Не пустой порядочный множитель без максимального элемента несомненно бесконечен: существует строго возрастающая последовательность в α, то есть отображение f: Nat → α с f(n) < f(n+1).
LaTeX
$$$\exists f: \mathbb{N} \to \alpha\text{ with } \forall n,\; f(n) < f(n+1)$$$
Lean4
/-- A nonempty preorder with no maximal element is infinite. -/
instance infinite [Nonempty α] [NoMaxOrder α] : Infinite α :=
let ⟨f, hf⟩ := Nat.exists_strictMono α
Infinite.of_injective f hf.injective
