exists_increasing_or_nonincreasing_subseq

English

For any transitive relation r, any sequence f has a subsequence g that is either strictly r-increasing or strictly reverts to non-increasing along the indices.

Русский

Для любого переходного отношения r любая последовательность f имеет подпоследовательность g, которая либо строго возрастает по r, либо после этого не сохраняется строгий рост.

LaTeX

$$$$\exists g:\mathbb{N} \hookrightarrow_o \mathbb{N},\ (\forall m n, m

Lean4

/-- This is the infinitary Erdős–Szekeres theorem, and an important lemma in the usual proof of
Bolzano-Weierstrass for `ℝ`. -/
theorem exists_increasing_or_nonincreasing_subseq (r : α → α → Prop) [IsTrans α r] (f : ℕ → α) :
    ∃ g : ℕ ↪o ℕ, (∀ m n : ℕ, m < n → r (f (g m)) (f (g n))) ∨ ∀ m n : ℕ, m < n → ¬r (f (g m)) (f (g n)) :=
  by
  obtain ⟨g, hr | hnr⟩ := exists_increasing_or_nonincreasing_subseq' r f
  · refine ⟨g, Or.intro_left _ fun m n mn => ?_⟩
    obtain ⟨x, rfl⟩ := Nat.exists_eq_add_of_le (Nat.succ_le_iff.2 mn)
    induction x with
    | zero => apply hr
    | succ x ih =>
      apply IsTrans.trans _ _ _ _ (hr _)
      exact ih (lt_of_lt_of_le m.lt_succ_self (Nat.le_add_right _ _))
  · exact ⟨g, Or.intro_right _ hnr⟩

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