exists_monotone_subseq — Mathlib

English

For any s that is PWOn, and any f: ℕ → α with values in s, there exists a monotone subsequence of f.

Русский

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

LaTeX

$$∀ {f : Nat → α}, (∀ n, f n ∈ s) → ∃ g : ℕ ↪o ℕ, Monotone (f ∘ g)$$

Lean4

nonrec theorem exists_monotone_subseq (h : s.IsPWO) {f : ℕ → α} (hf : ∀ n, f n ∈ s) : ∃ g : ℕ ↪o ℕ, Monotone (f ∘ g) :=
  h.exists_monotone_subseq hf

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