Theorems · Theorem · general topology

Filter.low_scores

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

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

Defined in

Mathlib.Order.Filter.AtTopBot.Finite

Cited by

0 results in Mathlib

Foundations

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

Assumes

LinearOrderNoMinOrder