Peak_Point_Lemma

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

limits-of-sequencesnamed-theoremspeak-point-lemmaproofwiki

Let $\sequence {x_n}$ be a sequence in $\R$ which is infinite. Then $\sequence {x_n}$ has an infinite subsequence which is monotone.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

import Mathlib.Analysis.Complex.Basic

theorem Peak_Point_Lemma (x : ℕ → ℝ) : ∃ phi : ℕ → ℕ, StrictMono phi ∧ (Monotone (x ∘ phi) ∨ Antitone (x ∘ phi)) := by sorry

Source

https://proofwiki.org/wiki/Peak_Point_Lemma

View graph