exists_strictMono — Mathlib

English

If α is nonempty and NoMaxOrder, there exists a strictly monotone function f: ℕ → α.

Русский

Если α непустое и нет максимального элемента, существует строго монотонная функция f: ℕ → α.

LaTeX

$$$[Nonempty α] [NoMaxOrder α] : \\exists f : \\mathbb{N} \\to α, \\mathrm{StrictMono} f$$$

Lean4

/-- If `α` is a nonempty preorder with no maximal elements, then there exists a strictly monotone
function `ℕ → α`. -/
theorem exists_strictMono [Nonempty α] [NoMaxOrder α] : ∃ f : ℕ → α, StrictMono f :=
  let ⟨a⟩ := ‹Nonempty α›
  let ⟨f, hf, _⟩ := exists_strictMono' a
  ⟨f, hf⟩

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