isPWO_iff_exists_monotone_subseq — Mathlib

English

The existence of a monotone subsequence is an equivalent characterization of being PWOn.

Русский

Существование монотонной подпоследовательности является эквивалентной характеристикой PWOn.

LaTeX

$$$s.PartiallyWellOrderedOn r \\iff \\forall f:\\\\mathbb{N} \\to \\alpha, (\\\\forall n, f n \\in s) \\\\to \\\\exists g : \\\\mathbb{N} ↪o \\\\mathbb{N}, \\\\forall m n, m ≤ n \\\\to r (f (g m)) (f (g n))$$$

Lean4

theorem isPWO_iff_exists_monotone_subseq : s.IsPWO ↔ ∀ f : ℕ → α, (∀ n, f n ∈ s) → ∃ g : ℕ ↪o ℕ, Monotone (f ∘ g) :=
  partiallyWellOrderedOn_iff_exists_monotone_subseq

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