Theorems · Theorem · general topology

Filter.high_scores

∀ {β : Type u_4} [inst : LinearOrder β] [NoMaxOrder β] {u : ℕ → β},
  Filter.Tendsto u Filter.atTop Filter.atTop → ∀ (N : ℕ), ∃ n ≥ N, ∀ k < n, u k < u n

If u is a sequence which is unbounded above, then after any point, it reaches a value strictly greater than all previous values.

Defined in

Mathlib.Order.Filter.AtTopBot.Finite

Cited by

2 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderNoMaxOrder