English
A relation r is a well-quasi-order iff for every sequence f: N → α, there exists a monotone subsequence g: N ↪o N such that for all m ≤ n, r(f(g(m)), f(g(n))).
Русский
Отношение r является хорошо-квазиупорядоченным тогда и только тогда, когда для любой последовательности f: нат. → α существует монотонная подпоследовательность g: нат. ↪о нат., и для всех m ≤ n верно r(f(g(m)), f(g(n))).
LaTeX
$$$\\mathrm{WellQuasiOrdered}(r) \\iff \\forall f:\\mathbb{N}\\to \\alpha,\\ \\exists g:\\mathbb{N}\\hookrightarrow_o \\mathbb{N},\\ \\forall m,n:\\mathbb{N},\\ m \\le n \\Rightarrow r\\bigl(f(g(m)), f(g(n))\\bigr)$$$
Lean4
theorem wellQuasiOrdered_iff_exists_monotone_subseq [IsPreorder α r] :
WellQuasiOrdered r ↔ ∀ f : ℕ → α, ∃ g : ℕ ↪o ℕ, ∀ m n : ℕ, m ≤ n → r (f (g m)) (f (g n)) :=
by
constructor <;> intro h f
· exact h.exists_monotone_subseq f
· obtain ⟨g, gmon⟩ := h f
exact ⟨_, _, g.strictMono Nat.zero_lt_one, gmon _ _ (Nat.zero_le 1)⟩
