exists_monotone_subseq — Mathlib

English

In a well-quasi-ordered set, every sequence has a monotone subsequence with respect to the order.

Русский

В хорошо упорядоченном множество каждая последовательность имеет монотонную подпоследовательность по отношению к порядку.

LaTeX

$$$\\exists g:\\mathbb{N} \\hookrightarrow_o \\mathbb{N},\\ \\forall m,n,\\ m \\le n \\Rightarrow r\\bigl(f(g(m)), f(g(n))\\bigr)$$$

Lean4

theorem exists_monotone_subseq [IsPreorder α r] (h : WellQuasiOrdered r) (f : ℕ → α) :
    ∃ g : ℕ ↪o ℕ, ∀ m n, m ≤ n → r (f (g m)) (f (g n)) :=
  by
  obtain ⟨g, h1 | h2⟩ := exists_increasing_or_nonincreasing_subseq r f
  · refine ⟨g, fun m n hle => ?_⟩
    obtain hlt | rfl := hle.lt_or_eq
    exacts [h1 m n hlt, refl_of r _]
  · obtain ⟨m, n, hlt, hle⟩ := h (f ∘ g)
    cases h2 m n hlt hle

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