infinite — Mathlib

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 αᵒᵈ _ _ _

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