exists_monotone_subseq — Mathlib

English

Let h be a PWOn on s; for any f: ℕ → α with values in s, there exists a monotone subsequence of f.

Русский

Пусть h — PWOn на s; для любой f: ℕ → α со значениями в s существует монотонная подпоследовательность f.

LaTeX

$$$\\forall f:\\\\mathbb{N} \\to \\alpha, (\\\\forall n, f(n) \\in s) \\\\to \\exists g : \\\\mathbb{N} \\hookrightarrow \\\\mathbb{N}, Monotone (f \\circ g)$$$

Lean4

theorem exists_monotone_subseq (h : s.PartiallyWellOrderedOn r) {f : ℕ → α} (hf : ∀ n, f n ∈ s) :
    ∃ g : ℕ ↪o ℕ, ∀ m n : ℕ, m ≤ n → r (f (g m)) (f (g n)) :=
  WellQuasiOrdered.exists_monotone_subseq h fun n ↦ ⟨_, hf n⟩

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