TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The limit superior is itself a subsequential limit in $\overline{R}$ and is the greatest one

Statement

Let $(x_{k})$ be a sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences) and write $Λ : = {lim sup}_{k} x_{k} \in \overline{R}$ (Limit superior and limit inferior of a real sequence as $\inf_{n} \sup_{k \geq n} x_{k}$ and $\sup_{n} \inf_{k \geq n} x_{k}$ in $\overline{R}$ ). Then, with the extended subsequential limit set $\overset{}{SL} (x)$ of Convergence in $\overline{R}$ and the extended subsequential limit set: $L \in \overline{R}$ is an extended subsequential limit when some subsequence converges to $L$ , or diverges to $L = \pm \infty$ :

$Λ \in \overset{}{SL} (x)$ : there is a strictly increasing $n : N \to N$ such that $(x_{n_{j}})$ converges to $Λ$ in $\overline{R}$ ;
$L \leq Λ$ for every $L \in \overset{}{SL} (x)$ .

So $\overset{}{SL} (x)$ is nonempty and has a greatest element, and that element is ${lim sup}_{k} x_{k}$ . In particular every sequence of reals whatever has a subsequence that converges in $\overline{R}$ .

The extended set is the right home for this statement, and the real set is not. The finite subsequential limit set $SL (x)$ of Subsequential limit of a real sequence, and the subsequential limit set may be empty, and when it is not it may have a greatest element different from ${lim sup}_{k} x_{k}$ ; both failures are exhibited by the dedicated counterexample on the companion page. What is true for $SL (x)$ follows: when $Λ$ is a real number, claim 1 puts it in $SL (x)$ , since the two sets agree on $R$ (Convergence in $\overline{R}$ and the extended subsequential limit set: $L \in \overline{R}$ is an extended subsequential limit when some subsequence converges to $L$ , or diverges to $L = \pm \infty$ ), and claim 2 then makes it the greatest element there too.

Facts & Assumptions

Given: A sequence $(x_{k})$ of reals, its tail ranges $T_{n} = {x_{k} : k \geq n}$ , the extended tail suprema $s_{n} = \sup T_{n}$ , and $Λ : = {lim sup}_{k} x_{k} = \inf {s_{n} : n \in N}$ (Limit superior and limit inferior of a real sequence as $\inf_{n} \sup_{k \geq n} x_{k}$ and $\sup_{n} \inf_{k \geq n} x_{k}$ in $\overline{R}$ ).

[L1]

All of $s_{n}$ and $Λ$ exist in $\overline{R}$ , with $s_{n}$ the least upper bound of $T_{n}$ and $Λ$ the greatest lower bound of ${s_{n}}$ (The tail suprema of any real sequence are nonincreasing in $\overline{R}$ , so the limit superior exists for every sequence, Every subset of $\overline{R}$ has a least upper bound and a greatest lower bound in $\overline{R}$ , agreeing with the real supremum and infimum on nonempty sets bounded in $R$ , Upper bound, least upper bound, and strict upper bound, Partial order and partially ordered set).

[L2]

The order on $\overline{R}$ is total, so the failure of $a \leq b$ is $b < a$ ; $- \infty$ is least and $+ \infty$ greatest; every real is $< + \infty$ and $> - \infty$ ; and on $R$ the order is that of $R$ (The extended real line $\overline{R} = R \cup {- \infty, + \infty}$ , its order, and the arithmetic that is left undefined, Partial order and partially ordered set).

[L3]

Epsilon characterisation for a real $Λ$ : for every real $η > 0$ one has $x_{k} < Λ + η$ eventually and $x_{k} > Λ - η$ frequently (For finite $L$ : $L = lim sup x_{k}$ iff for every $ε > 0$ one has $x_{k} < L + ε$ eventually and $x_{k} > L - ε$ frequently).

[L4]

Recursion theorem: for a set $A$ , an element $a \in A$ and a function $f : A \to A$ there is a unique $g : N \to A$ with $g_{0} = a$ and $g_{j + 1} = f (g_{j})$ (The recursion theorem).

[L5]

Well-ordering principle: every nonempty subset of $N$ has a least element (The well-ordering principle).

[L6]

Index maps: if $n_{j} < n_{j + 1}$ for every $j$ then $n$ is strictly increasing, and then $n_{j} \geq j$ for every $j$ ; the composite $(x_{n_{j}})$ is a subsequence (A strictly increasing index map satisfies $n_{k} \geq k$ , Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L7]

Convergence in $\overline{R}$ and the extended subsequential limit set (Convergence in $\overline{R}$ and the extended subsequential limit set: $L \in \overline{R}$ is an extended subsequential limit when some subsequence converges to $L$ , or diverges to $L = \pm \infty$ ); convergence to a real, for which it suffices to produce a threshold for every real $ε > 0$ (Limits and Cauchy sequences of reals, Sequences of reals: bounded, eventually, frequently, tails, subsequences); divergence to $\pm \infty$ (Divergence to $+ \infty$ and to $- \infty$ ); and $∣ a - b ∣ < c$ if and only if $b - c < a < b + c$ for $c > 0$ (Basic properties of the absolute value).

[L8]

If ${lim sup}_{k} x_{k} = - \infty$ then ${lim inf}_{k} x_{k} = - \infty$ and $x_{k} \to - \infty$ ( $lim inf x_{k} \leq lim sup x_{k}$ for every real sequence, A real sequence converges to $L \in R$ iff $lim inf x_{k} = lim sup x_{k} = L$ , and diverges to $\pm \infty$ iff both equal $\pm \infty$ ).

[L9]

Limits preserve non-strict inequalities: if $y_{j} \leq c$ for all large $j$ and $y_{j} \to y$ in $R$ , then $y \leq c$ (Limits preserve non-strict inequalities).

[L10]

Archimedean facts: for every real $M$ there is a natural $p \geq 1$ with $M < p \cdot 1_{R}$ , and for every real $η > 0$ a natural $m \geq 1$ with $1 / m < η$ ; the canonical naturals satisfy $0 \leq n \cdot 1_{R}$ and are increasing in $n$ , and $0 < a \leq b$ gives $0 < 1 / b \leq 1 / a$ (Every complete ordered field is Archimedean, For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Canonical naturals are positive and strictly increasing, Inverses of positives are positive, and reciprocation reverses order).

[L11]

Strictly between any two reals lies a rational, hence a real (The rationals embed densely in the reals).

[L12]

The order on $N$ is total and transitive, so any two indices have a common upper bound (Order on the natural numbers, $\leq$ is a linear order on $N$ ).

Proof

technique · constructive

1.1

The element $Λ = {lim sup}_{k} x_{k}$ exists in $\overline{R}$ , and exactly one of the following holds: $Λ$ is a real number, $Λ = + \infty$ , or $Λ = - \infty$ .

givenL1L2

1.2

Suppose $Λ = + \infty$ . Since $Λ$ is a lower bound of ${s_{n}}$ , every $n$ has $+ \infty \leq s_{n}$ and so $s_{n} = + \infty$ . Consequently, for every $n \in N$ and every real $M$ there is $k \geq n$ with $x_{k} > M$ : otherwise $M$ would be an upper bound of $T_{n}$ and leastness would give $s_{n} \leq M$ , contradicting $M < + \infty$ .

givenL1L2

1.3

Suppose $Λ$ is real. Then for every $n \in N$ and every real $η > 0$ there is $k \geq n$ with $∣ x_{k} - Λ ∣ < η$ : by [L3] fix $K$ with $x_{k} < Λ + η$ for all $k \geq K$ , let $K^{'}$ be an index at least as large as both $n$ and $K$ , and use that $x_{k} > Λ - η$ frequently to obtain $k \geq K^{'}$ with $x_{k} > Λ - η$ ; that $k$ satisfies $k \geq K$ , hence also $x_{k} < Λ + η$ , and $k \geq n$ .

givenL3L7L12

1.4

Suppose $Λ = - \infty$ . Then $x_{k} \to - \infty$ by [L8], and the identity map $j \mapsto j$ is strictly increasing, so the subsequence $(x_{j})$ of $(x_{k})$ converges to $- \infty$ in $\overline{R}$ and $Λ \in \overset{}{SL} (x)$ .

givenL6L7L8

1.5

Let $L \in \overset{}{SL} (x)$ be arbitrary and fix a strictly increasing $n : N \to N$ such that $(x_{n_{j}})$ converges to $L$ in $\overline{R}$ ; then $n_{j} \geq j$ for every $j$ .

givenL6L7

2.1

In the case $Λ = + \infty$ , define $f : N \to N$ by letting $f (n)$ be the least element of $E_{n} : = {k \in N : k > n and x_{k} > n \cdot 1_{R}}$ , which is nonempty by step 1.2 applied with the index $n + 1$ and the real $M = n \cdot 1_{R}$ , and let $a$ be the least element of ${k : x_{k} > 0}$ , nonempty by step 1.2 with $n = 0$ and $M = 0$ . Then $f (n) > n$ and $x_{f (n)} > n \cdot 1_{R}$ for every $n$ .

step 1.2L5construct

2.2

In the case $Λ$ real, define $g : N \to N$ by letting $g (n)$ be the least element of $F_{n} : = {k \in N : k > n and ∣ x_{k} - Λ ∣ < 1 / (n + 1)}$ , which is nonempty by step 1.3 applied with the index $n + 1$ and $η = 1 / (n + 1) > 0$ , and let $b$ be the least element of ${k : ∣ x_{k} - Λ ∣ < 1}$ , nonempty by step 1.3 with $n = 0$ and $η = 1$ . Then $g (n) > n$ and $∣ x_{g (n)} - Λ ∣ < 1 / (n + 1)$ for every $n$ .

step 1.3L5L10construct

2.3

If $L = - \infty$ then $L \leq Λ$ , since $- \infty$ is the least element of $\overline{R}$ .

step 1.5L2

2.4

If $L = + \infty$ , then for every real $M$ there is $J$ with $x_{n_{j}} > M$ for all $j \geq J$ . Fix $n \in N$ and a real $M$ , and take $j$ at least as large as both $J$ and $n$ ; then $n_{j} \geq j \geq n$ , so $x_{n_{j}} \in T_{n}$ and $M < x_{n_{j}} \leq s_{n}$ . As $M$ was an arbitrary real, $s_{n}$ is neither real nor $- \infty$ , so $s_{n} = + \infty$ ; as $n$ was arbitrary, $Λ = \inf {s_{n}} = + \infty$ and $L \leq Λ$ .

step 1.5L1L2L7L12

2.5

If $L$ is real, suppose for the sake of the comparison that $Λ < L$ . By step 1.1 the element $Λ$ is then real or $- \infty$ ; choose a real $c$ with $Λ < c < L$ , taking a rational strictly between $Λ$ and $L$ in the first case and $c : = L - 1$ in the second. Since $Λ$ is the greatest lower bound of ${s_{n}}$ and $Λ < c$ , the element $c$ is not a lower bound, so there is $n$ with $s_{n} < c$ , and then $x_{k} \leq s_{n} < c$ for every $k \geq n$ . For $j \geq n$ we have $n_{j} \geq j \geq n$ , hence $x_{n_{j}} \leq c$ , so $L \leq c$ by [L9], contradicting $c < L$ . By totality $L \leq Λ$ .

step 1.5step 1.1L1L2L9L11

3.1

In the case $Λ = + \infty$ , the recursion theorem applied to $N$ , the element $a$ and the function $f$ gives $n : N \to N$ with $n_{0} = a$ and $n_{j + 1} = f (n_{j})$ . Then $n_{j} < n_{j + 1}$ for every $j$ , so $n$ is strictly increasing and $n_{j} \geq j$ ; and $x_{n_{j + 1}} > n_{j} \cdot 1_{R} \geq j \cdot 1_{R}$ for every $j$ .

step 2.1L4L6L10

3.2

In the case $Λ$ real, the recursion theorem applied to $N$ , the element $b$ and the function $g$ gives $n : N \to N$ with $n_{0} = b$ and $n_{j + 1} = g (n_{j})$ . Then $n$ is strictly increasing with $n_{j} \geq j$ , and $∣ x_{n_{j + 1}} - Λ ∣ < 1 / (n_{j} + 1) \leq 1 / (j + 1)$ for every $j$ .

step 2.2L4L6L10

4.1

In the case $Λ = + \infty$ , the subsequence $(x_{n_{j}})$ diverges to $+ \infty$ : given a real $M$ , take a natural $p \geq 1$ with $M < p \cdot 1_{R}$ ; every $j \geq p + 1$ satisfies $j - 1 \geq p$ , so step 3.1 applied at $j - 1$ gives $x_{n_{j}} > (j - 1) \cdot 1_{R} \geq p \cdot 1_{R} > M$ . Hence $(x_{n_{j}})$ converges to $+ \infty = Λ$ in $\overline{R}$ and $Λ \in \overset{}{SL} (x)$ .

step 3.1L7L10L12

4.2

In the case $Λ$ real, the subsequence $(x_{n_{j}})$ converges to $Λ$ : given a real $ε > 0$ , take a natural $m \geq 1$ with $1 / m < ε$ ; every $j \geq m$ satisfies $j \geq 1$ , so step 3.2 applied at $j - 1$ gives $∣ x_{n_{j}} - Λ ∣ < 1 / j \leq 1 / m < ε$ . Producing such a threshold for every real $ε > 0$ establishes convergence, so $(x_{n_{j}})$ converges to $Λ$ in $\overline{R}$ and $Λ \in \overset{}{SL} (x)$ .

step 3.2L7L10

5.1

The three cases of step 1.1 are exhaustive, and each produces a subsequence converging to $Λ$ in $\overline{R}$ : step 4.1 when $Λ = + \infty$ , step 4.2 when $Λ$ is real, and step 1.4 when $Λ = - \infty$ . So $Λ \in \overset{}{SL} (x)$ , which is claim 1.

step 4.1step 4.2step 1.4L7

6.1

Steps 2.3, 2.4 and 2.5 cover the three possibilities for an arbitrary $L \in \overset{}{SL} (x)$ and give $L \leq Λ$ in each, which is claim 2. With claim 1 this makes $\overset{}{SL} (x)$ nonempty with greatest element $Λ = {lim sup}_{k} x_{k}$ .

step 5.1step 2.3step 2.4step 2.5L2discharge-construct∎

Remarks

The construction uses no choice. Both index maps are built by taking a least element (The well-ordering principle) of an explicitly described nonempty set of naturals, so the functions $f$ and $g$ are defined outright and The recursion theorem then produces the index map. This is the same device as in Every real sequence has a monotone subsequence (the peak / rising-sun lemma), and for the same reason: a subsequence selected by repeated arbitrary choices would need a choice principle, and none is needed here.
Why the recursion threshold is indexed by the previous index rather than by the step number. The recursion theorem produces a function of one variable, so the state carried from one step to the next is the index $n_{j}$ alone. Demanding $x_{n_{j + 1}} > n_{j}$ rather than $x_{n_{j + 1}} > j$ keeps that single-variable form, and $n_{j} \geq j$ (A strictly increasing index map satisfies $n_{k} \geq k$ ) then upgrades the bound to the one actually wanted. The same trick fixes the accuracy in the finite case at $1 / (n_{j} + 1) \leq 1 / (j + 1)$ .
Claim 2 is where the $lim sup$ earns the word "greatest". A subsequence cannot do better than the tail suprema allow: past any index $n$ , every term of the sequence, and so every term of any subsequence, is at most $s_{n}$ , and $Λ$ is the infimum of those. That is the entire content of step 2.5, and the strictness of the inequality $Λ < c$ is what gives the contradiction, since a limit inherits only the non-strict inequality (Limits preserve non-strict inequalities).
Both failures of the real version really occur, and A sequence with $lim sup = + \infty$ : the greatest subsequential limit exists only in $\overline{R}$ ↗ on the companion page is the witness: there $SL (x)$ is nonempty with greatest element $0$ while ${lim sup}_{k} x_{k} = + \infty$ .
The dual statement is The limit inferior is the least subsequential limit in $\overline{R}$ , obtained from this theorem by reflection rather than by repeating the construction.

Depends on

Used by

Dependency tree · two levels

62 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Limit superior and limit inferior (Wikipedia) (standard reference, not scraped)
Subsequential limit (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (3.17) (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §6.4 (standard reference, not scraped)
N. Donaldson, Math 140A: Real Analysis notes (standard reference, not scraped)

The limit superior is itself a subsequential limit in R‾R and is the greatest one