exists_increasing_or_nonincreasing_subseq'

English

For any r, any f: ℕ → α, there exists a subsequence g such that either it is strictly r-increasing along g, or it is not strictly r-increasing along g.

Русский

Для любого r и любой f: ℕ → α существует подпоследовательность g, такая что либо она строго возрастает по r вдоль g, либо не возрастает по r вдоль g.

LaTeX

$$$$\exists g:\mathbb{N} \hookrightarrow_o \mathbb{N},\ (\forall n, r(f(g(n)), f(g(n+1)))) \,\lor\, (\forall m,n, m

Lean4

theorem exists_increasing_or_nonincreasing_subseq' (r : α → α → Prop) (f : ℕ → α) :
    ∃ g : ℕ ↪o ℕ, (∀ n : ℕ, r (f (g n)) (f (g (n + 1)))) ∨ ∀ m n : ℕ, m < n → ¬r (f (g m)) (f (g n)) := by
  classical
  let bad : Set ℕ := {m | ∀ n, m < n → ¬r (f m) (f n)}
  by_cases hbad : Infinite bad
  · refine ⟨Nat.orderEmbeddingOfSet bad, Or.intro_right _ fun m n mn => ?_⟩
    have h := @Set.mem_range_self _ _ (↑(Nat.orderEmbeddingOfSet bad)) m
    rw [Nat.orderEmbeddingOfSet_range bad] at h
    exact h _ ((OrderEmbedding.lt_iff_lt _).2 mn)
  · rw [Set.infinite_coe_iff, Set.Infinite, not_not] at hbad
    obtain ⟨m, hm⟩ : ∃ m, ∀ n, m ≤ n → n ∉ bad :=
      by
      by_cases he : hbad.toFinset.Nonempty
      ·
        refine
          ⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
            Nat.not_succ_le_self _ (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩
      · exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩
    have h : ∀ n : ℕ, ∃ n' : ℕ, n < n' ∧ r (f (n + m)) (f (n' + m)) :=
      by
      intro n
      have h := hm _ (Nat.le_add_left m n)
      simp only [bad, exists_prop, not_not, Set.mem_setOf_eq, not_forall] at h
      obtain ⟨n', hn1, hn2⟩ := h
      refine ⟨n + n' - n - m, by cutsat, ?_⟩
      convert hn2
      omega
    let g' : ℕ → ℕ := @Nat.rec (fun _ => ℕ) m fun n gn => Nat.find (h gn)
    exact
      ⟨(RelEmbedding.natLT (fun n => g' n + m) fun n =>
            Nat.add_lt_add_right (Nat.find_spec (h (g' n))).1 m).orderEmbeddingOfLTEmbedding,
        Or.intro_left _ fun n => (Nat.find_spec (h (g' n))).2⟩

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