English
There exists a strictly monotone function f: ℕ → α with f 0 = a, assuming NoMaxOrder on α.
Русский
Существует строго монотонная функция f: ℕ → α с f(0) = a при условии NoMaxOrder на α.
LaTeX
$$$[NoMaxOrder \\ α] (a : α) \\Rightarrow \\exists f : \\mathbb{N} \\to α, \\mathrm{StrictMono} f \\land f 0 = a$$$
Lean4
/-- If `α` is a preorder with no maximal elements, then there exists a strictly monotone function
`ℕ → α` with any prescribed value of `f 0`. -/
theorem exists_strictMono' [NoMaxOrder α] (a : α) : ∃ f : ℕ → α, StrictMono f ∧ f 0 = a :=
by
choose g hg using fun x : α ↦ exists_gt x
exact ⟨fun n ↦ Nat.recOn n a fun _ ↦ g, strictMono_nat_of_lt_succ fun n ↦ hg _, rfl⟩
