partiallyWellOrderedOn_iff_exists_monotone_subseq

English

The PWOn property is equivalent to the existence, for every sequence in s, of a monotone subsequence.

Русский

Свойство PWOn эквивалентно тому, что для каждой последовательности в s существует монотонная подпоследовательность.

LaTeX

$$$s.PartiallyWellOrderedOn r \\leftrightarrow \\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 partiallyWellOrderedOn_iff_exists_monotone_subseq :
    s.PartiallyWellOrderedOn r ↔ ∀ f : ℕ → α, (∀ n, f n ∈ s) → ∃ g : ℕ ↪o ℕ, ∀ m n : ℕ, m ≤ n → r (f (g m)) (f (g n)) :=
  by
  use PartiallyWellOrderedOn.exists_monotone_subseq
  rw [PartiallyWellOrderedOn, wellQuasiOrdered_iff_exists_monotone_subseq]
  exact fun H f ↦ H _ fun n ↦ (f n).2

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