English
If α is a nonempty preorder with no minimal or maximal elements, then there exists a strictly monotone function f: ℤ → α.
Русский
Если α — непустое частично упорядоченное множество без минимального и максимального элементов, то существует строго монотонная функция f: ℤ → α.
LaTeX
$$$\\forall α\\,[Preorder α]\\,[Nonempty α]\\,[NoMinOrder α]\\,[NoMaxOrder α],\\ \\exists f:\\mathbb{Z} \\to α,\\ \\ StrictMono f.$$$
Lean4
/-- If `α` is a nonempty preorder with no minimal or maximal elements, then there exists a strictly
monotone function `f : ℤ → α`. -/
theorem exists_strictMono : ∃ f : ℤ → α, StrictMono f :=
by
inhabit α
rcases Nat.exists_strictMono' (default : α) with ⟨f, hf, hf₀⟩
rcases Nat.exists_strictAnti' (default : α) with ⟨g, hg, hg₀⟩
refine ⟨fun n ↦ Int.casesOn n f fun n ↦ g (n + 1), strictMono_int_of_lt_succ ?_⟩
rintro (n | _ | n)
· exact hf n.lt_succ_self
· change g 1 < f 0
rw [hf₀, ← hg₀]
exact hg Nat.zero_lt_one
· exact hg (Nat.lt_succ_self _)
